Reasoning with !-Graphs

tIOT:"WOE [OTSO] [^8Z8L*EOFT:^!XIP Alexander Merry Magdalen College University of Oxford
A thesis submitted for the degree of
Doctor of Philosophy
Trinity 2013

Acknowledgements

Firstly, I would like to thank my supervisors, Professor Samson Abramsky and Professor Bob Coecke, for giving me the opportunity to do this research and supporting me in my efforts, as well as for starting the field that was the motivation for this work. I also owe an immense debt of gratitude to Dr. Aleks Kissinger, who both paved the way for my work and gave me invaluable advice, encouragement and feedback on the way.
I wish to thank Dr. Lucas Dixon and Dr. Ross Duncan for the work they put into Quantomatic, both the theory and the implementation, without which this work could have taken much longer. Additionally, I owe thanks to Matvey Soloviev for his bright ideas in the DCM paper,which really opened up the possibility of reasoning about ! - graphs using graph rewriting.
Thanks also to the administrative staff of the Department of Computer Science for helping me navigate university bureaucracy, and especially to Julie Sheppard and Janet Sadler.
Finally, a huge thank you to my family and friends, who have supported and encouraged me over the last four years, through the hard times and the good. I couldn't have done it without you.

Abstract

The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories.
String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string graphs has provided a combinatorial formalisation of string diagrams, laying the foundations for this project.
The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning.
This dissertation firstly extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation - and structures to encode it - to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. This can be used to represent, for example, the "spider law" of CFAs, allowing two spiders to be merged, as well as the much more complex generalised bialgebra law that can arise from two interacting CFAs.
This work then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.

Contents

1 Introduction 1
2 Diagrammatic Reasoning 日 2.1 Monoidal Categories 2.2 Quantum Computation with Diagrams
3 Rewriting
3.1 Term Rewriting and the Word Problem
3.2 Monoidal Signatures
3.3 Graphs .
3.3.1 String Graphs .
3.4 Valuation
3.4.1 Framed String Graphs
3.4.2 Indexings and Contractions
3.4.3 Value
3.5 Graph Equations
3.5.1 Soundness
3.6 Graph Rewriting
3.6.1 Equational Reasoning with Rewrites
3.6.2 Matching up to Wire Homeomorphism
4 !-Graphs 57
4.1 Open Subgraphs 58
4.2 The Category of !-Graphs [60]
4.2.1 Wire Homeomorphisms 64
4.3 The !-Box Operations 64
4.4 Matching String Graphs With !-Graphs [69]
4.4.1 Nested and Overlapping !-boxes .
4.5 Related Work
5 !-Graph Rewriting 77
5.1 !-Graph Equations 77
T
5.2 Rewriting String Graphs with !-Graph Equations 85
5.3 Rewriting !-Graphs With !-Graph Equations . 85
5.4 Soundness of !-Graph Rewriting | 90
6 A Logic of !-Graphs 99
6.1 !-Graph Equational Logic |99|
6.2 Regular Forms of Instantiations 100
6.2.1 Depth-Ordered Form 101
6.2.2 Expansion-Normal Form 108
6.3 !-box Introduction 110
6.4 !-box Induction 112
6.4.1 The Generalised Bialgebra Law 117
6.5 Merging !-boxes 125
6.6 A More Traditional Logic 130
7 Computability of !-Graph Matching 135
7.1 Enumerating Instances 135
7.2 Matching in Quantomatic 138
7.2.1 Matching Onto !-Graphs 142
8 Conclusions and Further Work 147
8.1 Further Work 148
A Correctness of Quantomatic's Matching 151
B The Spider Law 163
Bibliography 168

Chapter 1

Introduction

In the early 1950s, as a research student attending lectures on differential geometry, Roger Penrose developed a pictoral notation for dealing with tensors. He started using this in publications some twenty years later, most notably in [32]. His motivation for using this notation was as an exposition and working aid when dealing with the tensor index notation common in various areas of physics. [32], in which Penrose generalised and formalised tensor index notation as abtract tensors, is liberally illustrated with these diagrams. In a tensor expression like
AnipBikkCplDmnq
where we can consider the large letters to be morphisms with subscripts as inputs and superscripts as outputs, we have to keep careful track of which indices are repeated (and therefore should be contracted - the notion of composition for abstract tensors). This is made clear in the following diagrammatic representation
These string diagrams (or wire diagrams) are particularly good at capturing information with a planar (or mostly planar), rather than linear, structure. Thus it was quite natural that they came to be used for monoidal categories,which have an associative,unital bifunctor :C×CC that acts as a form of composition orthogonal to the categorial composition.
Note that, unlike in the traditional diagrams of category theory, string diagrams represent morphisms as nodes and objects as wires. This allows categorical composition to be represented by joining wires, as in
while the monoidal composition can be represented via juxtaposition
Twenty years after Penrose's publication, Joyal and Street formalised the link between string diagrams and monoidal categories, at least in part 20. In particular, they showed that progressive plane diagrams, a generalised topological graph with directed wires that do not cross or have loops, exactly capture the axioms of monoidal categories. Additionally, they showed that allowing crossings captures the axioms of symmetric monoidal categories, which have a natural isomorphism witnessing that ABBA for all objects A and B ,and that other variations on these diagrams capture braided and balanced monoidal categories.
Joyal and Street planned a follow-up paper to treat non-progressive diagrams, such as those with loops, but this was never published. The link between these diagrams and either traced symmetric monoidal categories or compact closed categories (depending on the restrictions placed on the diagrams) was shown in [23].
We concentrate on traced symmetric monoidal categories and compact closed categories in this thesis. Selinger's survey paper 37 gives a more comprehensive overview of graphical languages for various types of monoidal categories.
These diagrammatic languages found a home in the study of quantum computer science, when in 2004 Samson Abramsky and Bob Coecke recast von Neumann's axiomatisation of quantum mechanics into category theory, allowing the use of string diagrams. The diagrams proved to be particularly helpful in illuminating the role of entanglement in various quantum mechanical and quantum informational protocols, and provided a grounding for intuition in something familiar (the physical manipulation of a diagram) for something that, at many times, appears to behave counter-intuitively (quantum mechanics).
In this setting, the wires of a string diagram represent quantum mechanical systems, and the nodes are operations on those systems. Of particular relevance to this thesis is the importance of commutative Frobenius algebras in these languages.
A Frobenius algebra in a monoidal category C consists of a monoid (A,μ,η) and a comonoid (A,δ,ϵ) on an object of C - the monoid being an associative multiplication operation μ:AAA with unit η:IA ,and the comonoid being its dual δ:AAA with counit ϵ:AI - that interact "nicely". Specifically, they obey the Frobenius law:
(1Aμ)(δ1A)=δμ=(μ1A)(1Aδ)
If we represent the monoid and comonoid graphically as (A,,!) and (A,,) ,then this law can be drawn
∴=x˙=v
Commutative Frobenius algebras (CFAs) are those whose monoid is commutative and comonoid is cocommutative. They have the property that the value of any connected (in the graphical language) network of components of a given CFA is determined purely by the number of inputs, outputs and loops it has. This gives rise to a consise and useful representation of a CFA, the "spider":
Loops are encoded in this representation as self-loops (by connecting outputs to inputs).
This leads to the spider law, which allows us to merge two connected spiders of the same type
and this law significantly simplifies working with these graphical languages.
While the use of string diagrams can help greatly with understanding and intuition, constructing large proofs by hand can still be tedious and error-prone. This is where projects like Quantomatic [25], a collection of automated tools for graphical languages, come in.
The goal of Quantomatic is to produce a useful proof assistant for graphical languages; as its name suggests, it was originally aimed at the languages being developed for quantum computation. For example, Dixon and Duncan used it to verify the correctness of the Steane code in [12]. It is still primarily used for quantum languages, but it aims to be useful in other fields as well.
Dixon, Duncan and Kissinger provided a theoretical underpinning for Quantomatic's automated reasoning in the form of string graphs, introduced as open graphs in [10] and further refined by Dixon and Kissinger in [11] and then by Kissinger in [23]. These represent string diagrams as typed graphs, where the vertex types are sorted into node-vertices and wire-vertices, the former being the "real" vertices from the string diagram and the latter a kind of "dummy" vertex holding the wires in place (as well as carrying the wire type). For example, the string diagram
could be represented by the graph
This allows us to do equational reasoning for diagrams using graph rewriting, in a similar manner to how traditional proof assistants use term rewriting.
Note that string graphs are not the only combinatorial representation for the categorical structures that underlie string diagrams. In particular, Hasegawa, Hofmann and Plotkin use a bijective map to describe the connections formed by wires in their paper showing that finite dimensional vector spaces are complete for traced symmetric monoidal categories 18. Using graphs, however, allows us to build on a substantial body of established work on graph rewriting.
The first aim of this dissertation is to extend this formalism to allow tools like Quantomatic to work with the spider law and other,more complex,rules using the !-graphs posited in [9] as graph patterns. In particular, we aim to give a mathematical underpinning to these, which were previously only treated informally.
!-graphs are string graphs with demarked subgraphs called !-boxes that can be repeated any number of times, allowing an infinite family of graphs to be represented as a single graph:
This can be extended to string graph equations, allowing the spider law to be represented as a
!-graph equation:
We call a string graph or string graph equation represented by a !-graph or !-graph equation an instance of that graph or rule.
This notation may seem overpowered for simply representing the spider law, but it also allows many equations describing interactions between certain kinds of CFA, such as
which can be represented
and even more complex examples that we will describe in later chapters.
The second aim of this dissertation is to provide the beginnings of a formal system for reasoning about (and not just with) these !-graphs. We show that rewrite rules composed of !-graphs can be used to rewrite !-graphs and, in doing so, perform equational reasoning on these infinite families of string graphs. What is more, we introduce some additional rules to this logic of !-graphs, including a form of graphical induction that encodes inductive proofs that could previously only be done with a mix of diagrams and explanatory text.
Chapter 2 describes various types of monoidal category and the graphical languages they induce. It also provides some motivating examples in the form of a subset of the Z/X calculus for quantum information processing.
Chapter 3 provides a brief introduction to rewriting as a way of doing equational reasoning, using the well-established field of term rewriting. It then presents an equational logic for traced symmetric monoidal categories and compact closed categories using string graphs, and shows how this can be implemented using string graph rewriting. We present a slightly different construction of string graphs to [23], as Kissinger's construction does not allow for variable-arity nodes, required by the spiders of the quantum graphical languages.
Chapter 4 describes the !-box notation and its encoding in !-graphs. It provides a set of operations on ! -boxes (COPY,DROP and KILL) that are used to define the concrete instances of a ! -graph (ie: those string graphs it represents).
Chapter 5 introduces !-graph equations to represent families of string graph equations, and demonstrates how their directed form, !-graph rewrite rules, can be used to rewrite not only string graphs but also ! -graphs. The latter produces further ! -graph equations that are sound with respect to their interpretation as families of string graph equations. This effectively allows us to rewrite a potentially infinite family of string graphs simultaneously.
Chapter 6 builds on this to construct a nascent logic for reasoning about !-graphs. In particular, we construct an analogue of induction for string graphs which functions as a !-box introduction rule, and demonstrate how this can be used to derive
in the Z/X calculus. We also demonstrate a derivation of the generalised bialgebra law,which we introduce at the end of chapter 2
Chapter 7 demonstrates an algorithm for finding instances of !-graphs that match string graphs or other ! -graphs,allowing for practical implementations of rewriting with ! -graph rewrite rules. The complete matching process implemented in Quantomatic for rewriting string graphs with !- graph rewrite rules is described, as well as the planned extension to it that will allow !-graphs to be rewritten.
Finally, chapter 8 presents our conclusions and areas of further work.

Chapter 2

Diagrammatic Reasoning

This chapter provides a brief summary from the existing literature of various types of monoidal categories that are relevant to this thesis, and the diagrammatic representations of their morphisms. It also demonstrates their utility in reasoning about such categories using examples drawn from existing work in the area of graphical languages for quantum computation.

2.1 Monoidal Categories

Monoidal categories provide a useful setting for reasoning about processes of all kinds. In addition to the usual functional composition, they allow a form of parallel composition via the tensor product.
Definition 2.1.1 (Monoidal Category). A monoidal category is a category M equipped with
  • a bifunctor :M×MM ,called the tensor product;
  • a distinguished object I of M ,called the tensor unit; and
  • three natural isomorphisms
αA,B,C:(AB)CA(BC)
λA:IAA
ρA:AIA
where λI=ρI and the following diagrams commute:
((AB)C)Dα(AB)(CD)αA(B(CD))
Example 2.1.2. The category Set of sets is monoidal,with the cartesian product as and the single-element set as I . Alternatively,the disjoint union of sets and the empty set can be used as the monoidal structure.
The category VectK of vector spaces over a field K and linear functions between them is a monoidal category,where is the tensor product of vector spaces,and I is K as a one-dimensional vector space.
In later examples,we will use the fact that if U,V and W are vector spaces over K ,then each bilinear map f:U×VW induces a unique linear map f~:UVW . We can use this to construct the natural isomorphisms αU,V,W,λV and ρV from the maps
((u,v),w)u(vw) (k,v)kv (v,k)kv
When considering (categorical) diagrams of a monoidal category M involving the above isomorphisms, Mac Lane's coherence theorem 29 allows us to work instead in a category where those isomorphisms are identities; we call this category the strictification of M . Formal categorical diagrams (of the sort seen in definition 2.1.1) commute in M if and only if they commute in its strictification. Therefore, we abuse notation slightly by omitting paretheses and, insofar as possible, I ,writing
ABC
instead of
(AI)(BC)
for example.
In [32], Penrose presented a graphical language he had developed for representing tensor networks. Restricted variants of this language can be used for talking about more general monoidal categories.
In this notation, we represent objects of the category (and identity morphisms on those objects) as lines,and morphisms as boxes,also called nodes. For example,the morphism f:AB could be depicted
where we read the diagram in a downwards direction. The tensor product is depicted by placing things side-by-side,so if g:BC then fg:ABBC is and gf:AC is
One convenience that this immediately provides, other than requiring less mental effort to parse than conventional symbolic notation, is that the equation
(g1g2)(f1f2)=(g1f1)(g2f2)
  • a consequence of the fact that is a bifunctor - is implicit in the graphical notation; both sides of the equation are, in fact, represented by the same diagram
The tensor product has a rigid order; it is common to allow more flexibility, in a manner akin to rerouting information. This is provided by a symmetric monoidal category.
Definition 2.1.3 (Symmetric Monoidal Category). A symmetric monoidal category, or SMC, is a monoidal category M equipped with a natural isomorphism
γA,B:ABBA
such that γA,BγB,A=1,ρA=λAγA,I and the following diagram commutes:
Example 2.1.4. Set with either cartesian products or disjoint unions is symmetric,as is VectK . In the latter case, γ can be defined (see example 2.1.2) using the map
(v,w)(wv)
Diagrammatically,we represent γA,B as
The fact that γ is a natural isomorphism is represented in this notation as an ability to "slide" morphisms up and down wires:
Joyal and Street presented 20 a formalisation of Penrose's diagrams based on topological graphs. They showed that progressive polarised diagrams, essentially those without loops, can be used to form free symmetric monoidal categories; effectively, they exactly capture the axioms of a symmetric monoidal category.
There are plenty of scenarios where we do want to introduce loops, whether to represent the trace (or partial trace) operation on a matrix, looping in a computation or even the effects of entanglement in a quantum mechanical system, where information can sometimes appear to flow backwards in time.
A trace operation, if one exists, can be used to capture a looping construction.
Definition 2.1.5 (Traced Symmetric Monoidal Category). A traced symmetric monoidal category is a symmetric monoidal category M together with a trace operation: a function
TrA,BX:homM(AX,BX)homM(A,B)
for all objects X,A,B that satisfies the following conditions:
  1. TrX((g1X)f(h1X))=gTrX(f)h
  1. TrY(f(1Ag))=TrX((1Bg)f)
  1. TrI(f)=f
  1. TrXY(f)=TrX(TrY(f))
  1. TrX(gf)=gTrX(f)
  1. TrX(γX,X)=1X
Example 2.1.6. Vect K is a traced symmetric monoidal category,with the partial trace of linear maps as the trace operation.
TrA,BX(f) is represented as
and, as before, the properties of the trace operation are subsumed into its representation in the graphical language, either directly (as with 4 or 5 , for example, where both sides of the equation have the same representation) or via "natural" graphical manipulations. For example, condition 2 corresponds to sliding a morphism round a trace loop from one end to the other: although care must be taken, as the following diagram has no meaning in a traced SMC:
(but see remark 2.1.10 below). Condition 6 is visually represented as an ability to "yank" loops with no (non-identity) morphisms straight:
Finally, we come to compact closed categories. These are based around dual objects, which are the categorisation of dual spaces from linear algebra.
Definition 2.1.7 (Dual Objects). Let A and A be objects in a monoidal category. A is called a left dual of A (and A a right dual of A ) if there exist morphisms dA:AAI and eA:IAA such that
(dA1A)(1AeA)=1A
and
(1AdA)(eA1A)=1A
Note that in a symmetric monoidal category,if A is a left dual of A ,it is also a right dual of A and vice versa,so we simply say that A is the dual of A .
Definition 2.1.8 (Compact Closed Category). A compact closed category is a symmetric monoidal category where every object has a dual.
We add the notion of dual objects to the graphical language using arrows. If an object A is represented by a downward-directed wire, its dual is represented by an upward-directed one. The maps dA and eA can then be drawn
() and
respectively. The equations in the above definition can then be drawn
↓↑=↓ and ↑↓↓=↑
Example 2.1.9. Consider a finite-dimensional vector space vector space V and its (algebraic) dual space, V . Given a basis {u1,,un} of V ,there is a corresponding basis {u1,,un} of V such that
ui(a1u1++anun)=ai
We can then define the map dV:VVK to be induced (see example 2.1.2) by
(v,f)f(v)
and eV:KVV to be
kk(u1u1++unun)
So if we consider V as an object of FDVectK ,the category of finite-dimensional vector spaces over K,V is a categorical dual of V . Thus FDVectK is compact closed (although VectK is not). Note,however,that our definitions of dV and eV are not the only possibilities.
Given the graphical notation, we would expect to be able to construct a trace operation using these maps; this is indeed the case 21. TrA,BX(f) is
(1BdX)(f1X)(1AeX)
or, graphically,
Remark 2.1.10. Joyal, Street and Verity's Int construction 21 allows a traced SMC to be embedded in a compact closed category with formal dual objects. This allows the diagrams for compact closed categories to be given meaning when working with traced SMCs.

2.2 Quantum Computation with Diagrams

An area which is making active use of these diagrammatic languages is quantum information processing. Starting with a paper by Abramsky and Coecke in 2004 1, there has been considerable work in axiomatising quantum mechanics in a categorical setting that admits diagrammatic reasoning. Indeed, a major application of the ideas set out in this thesis is to make this work easier. We will therefore present a brief introduction to one of these languages, both as motivation and as a source of examples.
Most of the languages that have been developed in this area are based on compact closed categories; in particular, the usual model for them is the category FDHilb of finite dimensional Hilbert spaces.
Definition 2.2.1. A Hilbert space is a real or complex inner product space that is a complete metric space with respect to the distance metric
d(x,y)=xy,xy
Note that we can ignore the compactness requirement, as it is satisfied by all finite-dimensional inner product spaces.
FDHilb is a compact closed category,with the categorical dual of a Hilbert space H being the algebraic dual H ,as in FDVect (example 2.1.9). As such,we can make use of the diagrammatic language already introduced for such categories.
A structure that has particular importance in this formulation of quantum mechanics is the Frobenius algebra, a monoid and comonoid pair that interact particularly well.
A monoid in a monoidal category C as a triple (A,μ,η) where A is an object of C ,and μ : AAA and η:IA are morphisms satisfying unit and associativity laws:
μ(η1A)λA1=1A=μ(1Aη)ρA1
μ(μ1A)=μ(1Aμ)
Graphically,we can represent the monoid as (A,,!) ; these laws can then be drawn
y=1=v
and
y=y
A comonoid is the dual of this: a triple (A,δ,ϵ) with δ:AAA and ϵ:AI satisfying counit and coassociativity laws:
λA(ϵ1A)δ=1A=ρA(1Aϵ)δ
(δ1A)δ=(1Aδ)δ
Graphically,this is (A,A,δ) satisfying
λ=1=λ
and
=
A monoid and comonoid on the same object form a Frobenius algebra if they satisfy the Frobenius
law:
∴=12=1
or, symbolically,
(1Aμ)(δ1A)=δμ=(μ1A)(1Aδ)
A Frobenius algebra is commutative if the monoid is commutative and the comonoid is cocommu-
tative:
x=xy=xz=yz=z
μ=μγA,Aδ=γA,Aδ
Commutative Frobenius algebras (CFAs) appear repeatedly in quantum graphical languages, whether to describe entanglement [5, 6] or classical data 8. Thus the practical utility of these languages is greatly improved by a consequence of the Frobenius law, namely that any connected (in the diagrammatic language) network of multiplications, comultiplications, units and counits of a commutative Frobenius algebra has a unique normal form consisting of a series of multiplications followed by a series of loops followed by a series of comultplications:
This allows a more compact representation, generally referred to as a "spider":
where the loops are encoded by connecting outputs of the spider to inputs. Note that our original multiplication, comultiplication, unit and counit are subsumed into this notation. This leads to the spider law, which allows us to merge two connected spiders of the same type
The spider law and the spider identity law
completely capture the laws of a CFA.
There are various quantum graphical languages built around CFAs, including the Z/X calculus [5], the trichromatic calculus 28 and the GHZ/W calculus 6 . There are also several languages built on top of the Z/X calculus,such as Duncan and Perdrix’s calculus for measurement-based quantum computation 13. The GHZ/W calculus even admits an encoding of rational arithmetic [7].
We will use a restricted version of the Z/X calculus (without angles or scalars) to provide motivating examples. This consists of two special CFAs, called the X and Z CFAs, together with certain rules governing their interaction.
Definition 2.2.2. A CFA (,,$) is special if it satisfies
The "spiderised" version of this is
Traditionally,the X CFA has been represented with red nodes,and the Z CFA with green nodes. However, we will follow [23] in using grey for X and white for Z, if only to spare colourblind readers some frustration. Thus our CFAs are
(μX,ηX,δX,ϵX)=(,ϱ,δ,δ)
and
(μZ,ηZ,δZ,ϵZ)=(4,9,8,8)
In addition to the laws of a special CFA for each colour of node, we have the following laws:
x=0y=0z=000000000000000000000000000000000000000000000000000000000000000
0=00=0=0=0
We name these laws,for ease of reference, Z copies X,X copies Z ,the bialgebra law,scalar elimination and the dual law, in order.
For the dual law we might expect certain symmetries:
Indeed, we can use the laws of a CFA together with the dual law to derive these. For example, the last one can be derived as follows:
This fairly simple proof can be written in "traditional" mathematical notation as well, but - because we have to explicitly use various laws and axioms that are inherent in the diagrammatic language - it ends up being long and tedious. We present such a proof below to demonstrate this. For reference, the dual law written symbolically is
ρ(1A(ϵXμX))((δZηZ)1A)λ1=1A
Then we have
1A={(co) unitality laws }
μX(1AηX)ρ1λ(ϵX1A)δX
μZ(1AηZ)ρ1λ(ϵZ1A)δZ
={naturality ofλ,ρ}
λ(1IμX)(1I1AηX)(ϵX1A1I)(δX1I)ρ1
λ(1IμZ)(1I1AηZ)(ϵZ1A1I)(δZ1I)ρ1
={ bifunctoriality of }
λ(ϵX1A)(1AμX)(δX1A)(1AηX)ρ1
λ(ϵZ1A)(1AμZ)(δZ1A)(1AηZ)ρ1
={Frobenius law}
λ(ϵX1A)(μX1A)(1AδX)(1AηX)ρ1
λ(ϵZ1A)(μZ1A)(1AδZ)(1AηZ)ρ1
={ bifunctoriality of }
λ((ϵXμX)1A)(1A(δXηX))ρ1
λ((ϵZμZ)1A)(1A(δZηZ))ρ1
={ naturality of λ,ρ}
λ(1Iλ)(1I(ϵXμX)1A)(1I1A(δXηX))
((ϵZμZ)1A1I)(1A(δZηZ)1I)(ρ11I)ρ1
={ bifunctoriality of }
λ((ϵZμZ)1A)(1A1Aλ)(1A1A(ϵXμX)1A)
(1A(δZηZ)1A1A)(ρ11A1A)(1A(δXηX))ρ1
={ laws of λ,ρ}
λ((ϵZμZ)1A)(1Aρ1A)(1A1A(ϵXμX)1A)
(1A(δZηZ)1A1A)(1Aλ11A)(1A(δXηX))ρ1
={ bifunctoriality of }
λ((ϵZμZ)1A)
(1A(ρ(1A(ϵXμX))((δZηZ)1A)λ1)1A)
(1A(δXηX))ρ1
={dual law}
λ((ϵZμZ)λ)
(1A1A1A)
(ρ1(δXηX))ρ1
={identity}
λ((ϵZμZ)λ)(ρ1(δXηX))ρ1
Even with explanatory notes about what law is being used when, this proof is hard to follow - and was hard to construct - compared to the graphical notation.
Note that we can make the graphical version even cleaner by using spider notation:
The other two symmetries rely on commutativity. In particular, we have
and similarly with the colours swapped.
We can create "spiderised" versions of the copying laws
and we can prove that these are correct by induction on n . The proof is fairly simple,and we will just do the X copies Z version,since the other is symmetric. The base case (n=0) follows by the scalar elimination laws. So consider n=k+1 :
We can construct a similarly spiderised version of the bialgebra law with some trivial applications of the spider law
but there is also a generalised version of this involving the (s,t) -bipartite graph of X and Z spiders (the normal bialgebra law is the case when s=t=2 ). Graphically,this looks something like
but it is hard to see what this is supposed to represent without an accompanying textual description. For the same reason, proving this graphically is a messy affair, and convincing yourself that such a proof is correct is even harder.
Chapters 4 and 5 will introduce a formal notation capable of expressing this generalised bialgebra law, and chapter [6] will provide the techniques necessary to prove it formally, together with an informal demonstration of the proof.

Chapter 3

Rewriting

Equational reasoning is core to many problems in mathematics and computer science, from proving that a left unit is a right unit in a commutative ring to optimising functional programs.
The traditional approach to mechanising equational reasoning is to use term rewriting to implement equational logic. We will briefly describe this approach before presenting a related mechanisa-tion scheme, adapted from the existing literature (and [23] in particular), that is much more suited to the examples in the preceeding chapter.

3.1 Term Rewriting and the Word Problem

In order to reason formally about mathematical equations, we need a symbolic language to express those equations. This section summarises the relevant parts of a large body of existing literature on term rewriting and universal algebra; a more comprehensive introduction can be found in [3].
A signature provides symbols for the "fixed" elements of a theory: for example, a multiplication operator or its unit. It is simply a set of symbols ,each with an associated non-negative integer known as the arity 1 . In the case of group theory,we might have ={e,i,m} ,with respective arities 0,1 and 2 .
If we also have a set of variables V disjoint from ,we can start to write down terms such as m(i(x),e) (where x is a variable). The set of possible -terms over V,T(,V) ,is defined inductively:
  • if xV then xT(,V)
  • if f with arity n and t1,,tnT(,V) then f(t1,,tn)T(,V)
We can now encode equations using terms. A -equation is just a pair of terms that we wish to consider equal. We write such equations st ,where s and t are -terms,to make it clear that s and t are not the same term,but should be considered equal in the theory.

1 For simplicity,we are presenting untyped terms here

The axioms of our theory,for example the axioms of a group,are encoded as a set of -equations, and equational logic 17 describes how we can use those axioms to derive further equalities via the following inference rules, adapted for the notion of signature we are using in [3]
(Axiom)stEEst(Refr.)Ett(Sym)EstEts
(TRANS)EstEtuEsu(SUBST)EstEσ(s)σ(t)
(LEIBNIZ)Es1t1EsntnEf(s1,,sn)f(t1,,tn)
where σ is a substitution that replaces variables with other terms and f is an n -ary function symbol of .
We commonly wish to determine whether two -terms s and t are equal by this logic under a certain set of axioms E ; in other words,is it the case that Est ? This is known as the word problem and is a major application of term rewriting.
The obvious way to approach the word problem is to attempt to use the rules to construct a proof that two terms are equal directly. Term rewriting, in constrast, turns one term into another term that is equal according to the Axiom, SUBST and LEIBNIZ rules. This is done by directing equations st to make them rewrite rules,written st .
A set of terms E can be turned into a term rewrite system R in this way,and we define the relation R such that sRt if and only if there is a substitution σ and a rewrite rule lr in R such that σ(l) occurs in s ,and replacing that occurrence by σ(r) yields t . For example,if m(e,x)xR ,then we can deduce that
i(m(e,i(y)))Ri(i(y))
Matching is the process of finding an appropriate substitution σ and locating occurences of σ(l) in s ,and is decidable. Hence,given a finite set of rewrite rules R and a term s ,it is possible to find all terms t such that sRt .
The utility of this approach comes from the observation that the reflexive, symmetric, transitive closure of R - which we write R - corresponds exactly to the of equational logic; in other words,if we allow ourselves to view R as a set of equations,
sRtRst
This observation means,in particular,that if we can find a common term u such that sRu and tRu (where R is the transitive closure of R ),then we can deduce that Rst . For term rewrite systems that are terminating (there is no infinite chain s1Rs2R ) and confluent (if sRt1 and sRt2 then there is a term u such that t1Ru and t2Ru ),the word problem is decidable.
While terms, which can have multiple inputs (the variables) but only one output, are well-suited for encoding algebras, they are less useful for structures like coalgebras, where we can have multiple outputs. For example,while a multiplication map m:AAA in a monoidal category is easy to represent as a binary term,a comultiplication map d:AAA does not have such a clear symbolic representation.
Taking our cue from the diagrams of chapter 2 we will use graphs to construct a combinatorial symbolic representation of the sort of maps found in a monoidal category.

3.2 Monoidal Signatures

As with term rewriting, we need a way to represent items of interest from the theory we are reasoning about; in this case, these items correspond to objects and morphisms in a monoidal category.
Definition 3.2.1 (Monoidal Signature: [23], pp 30). A (small, strict) monoidal signature (O, M, dom, cod) consists of two sets M and O together with a pair of functions dom,cod : MO into lists of elements of O .
The intended interpretation of a monoidal signature is that the elements of O are representations of objects of a monoidal category, M is (some of) its morphisms and dom and cod give the types of the domain and codomain of the morphisms. An empty list corresponds to I ,the tensor unit.
Definition 3.2.2 (Monoidal Homomorphism: [23],pp 31). If S and T are monoidal signatures,a monoidal signature homomorphism f:ST consists of functions fO:OSOT and fM:MS MT making the following diagrams commute:
Recall from chapter 2 the "spiders" that arise from Frobenius algebras. These are families of morphisms that differ only in how many inputs or outputs of a certain type they have. Rather than having an infinite monoidal signature with an object in M for each possible combination of inputs and outputs, it would be useful to have a single symbol with variable arity. To this end, we adapt the definition of a monoidal signature:
Definition 3.2.3 (Compressed Monoidal Signature). If O and M are sets and dom,cod : M(O× {,}) are functions into lists of pairs of elements of O and either or ,then (O,M,dom,cod) is a compressed monoidal signature.
and are intended to indicate whether the input or output is of variable or fixed (single,in fact) arity. If it has variable arity, it can be removed or duplicated.
Of course, if this is to be a true compressed representation of a larger monoidal signature, we need a way to reconstruct that monoidal signature from the compressed version.
Definition 3.2.4 (Expansion). Let S=(O,M,dom,cod) be a compressed monoidal signature.
For each fM ,let Df be the indices of the -tagged elements of dom(f) ,and Cf the indices of the -tagged elements of cod(f) . The expansion of S , expn(S) ,is (O,M,dom,cod) where
-M={{f}×NDf×NCf:fM}
  • dom(f,df,cf) be dom(f) with,for all indices i ,the i th element replaced with x if it is (x,) and df(i) copies of x if it is (x,)
  • cod(f,df,cf) be cod(f) with,for all indices i ,the i th element replaced with x if it is (x,) and cf(i) copies of x if it is (x,)
S is said to be a compressed monoidal signature for a monoidal signature T if the expansion of S is isomorphic to T . Compressed monoidal signatures that make no use of correspond exactly to ordinary monoidal signatures.
Example 3.2.5. Consider the compressed monoidal signature where
O={A,B}
M={f,g}
dom(f)=[(A,)]
dom(g)=[(A,),(B,)]
cod(f)=[(A,),(A,)]
cod(g)=[(A,)]
To make the description simpler, and more evocative of the intended interpretation, we use the following notation:
f:[A][A,A]
g:[A,B][A]
The expansion of this signature would include
(f,10,):[][A,A]
(f,11,):[A][A,A]
(f,12,):[A,A][A,A]
and
(g,,20):[A][A]
(g,,21):[A,B][A]
(g,,22):[A,B,B][A]
Since the elements of a compressed monoidal signature are meant to represent families of morphisms in a category, we need a way of determining which morphisms they are supposed to represent. This is provided by a valuation.
Note: if X is a list,we use I(X) to refer to the set of indices of X .
Definition 3.2.6 (Arity Count). Let (M,O,dom,cod) be a compressed monoidal signature and fM . Then an arity count for f is a pair of maps d:I(dom(f))N and c:I(cod(f))N such that the index of each -tagged element maps to 1 .
Definition 3.2.7 (Valuation). A valuation v of a compressed monoidal signature (M,O,dom,cod) over a monoidal category C is a map vo from O to the objects of C together with a map vmf for each fM that takes arity counts for f to morphisms of C with
vmf(d,c):vo(α1)d(1)vo(αl)d(l)vo(β1)c(1)vo(βn)c(n)
where dom(f)=[α1,,αl],cod(f)=[β1,,βn],A0 is the monoidal identity I ,and An+1= AAn .
The valuation is said to be expansion-order invariant if V is a symmetric monoidal category and for all fM and all arity counts (d,c) for f ,if i is the index of a variable-arity entry of dom(f) and 1j<d(i) ,then
vmf(d,c)swapi,j=vmf(d,c)
where swapi,j is the map
1X1d(1)1Xi1d(i1)1Xij1γXi,Xi1Xid(i)j11Xi+1d(i+1)1Xld(l)
where Xi=vo(αi) ,and
swapi,jvmf(d,c)=vmf(d,c)
where i,j and swapi,j are defined analagously for cod(f) and c .
Expansion-order invariance is intended to capture the idea that, in the expansion of a compressed monoidal signature,a morphism should be commutative on the inputs derived from the same - tagged input,and cocommutative on outputs derived from the same -tagged output.
Example 3.2.8. Suppose we have a CFA (page 13) on an object X of a symmetric monoidal category
μ:XXX
η:IX
δ:XXX
ϵ:XI
and the compressed monoidal signature
s:[A][A]
If we want s to represent the spiderised version of the CFA,we can construct a valuation v such that vo(A)=X and vms(1k,1l) is k1 copies of μ followed by l1 copies of δ ,arranged in the following form:
If k=0 ,we use η to get a domain of I ,and if l=0 we use ϵ to get a codomain of I .
This valuation is expansion-order invariant because CFAs are (co-)commutative and (co-)associative, so precomposing or postcomposting the map above with swap maps does not affect the value of the morphism.

3.3 Graphs

A well-established categorical construction for directed graphs is to use functors into Set, the category of (small) sets:
Definition 3.3.1. Graph is the category of functors from the category
EtsV
to Set.
Each element of Graph therefore consists of two sets,one of edges (the image of E ) and one of vertices (the image of V ),and a pair of functions selecting the source (s) and target (t) of each edge. We say that an edge is incident to both its source and its target, and call the set of edges incident to a vertex vV the edge neighbourhood of v,E(v) . Also,the source of an edge is adjacent to its target, and vice versa.
We can separate vertices and edges into types through the use of a typegraph. This also allows the possible sources and targets of the edges to be constrained. For a given graph G ,we can construct the category Graph/G ,the slice category over G . The elements of this category can be viewed as pairs (H,tH) of a graph H and a graph morphism tH:HG ,known as the typing morphism, and the morphisms of the category are those graph morphisms f:GH that respect the typing morphisms, in the sense that
commutes. We call (H,tH) a G -typed graph.
If G is a subgraph of H ,then any G -typed graph can be viewed as a H -typed graph,simply by reinterpreting the codomain of the typing function (or, equivalently, composing the typing function with the embedding morphism from G to H ). The general theorem,stated in categorical terms,is as follows:
Theorem 3.3.2. Let C be a category,and m:ST a monomorphism in C . Then m induces a full embedding functor Em:C/SC/T . If C has pullbacks along monomorphisms, Em has a right adjoint Um ,and UmEm is the identity functor.
Proof. If (X,τX) is an object of C/S ,we define Em(X,τX)=(X,mτX) ,and let Em be the identity on morphisms. Recall that a morphism f:XY of C is a morphism f:(X,τX)(Y,τY) of C/S if and only if
τYf=τX
But if this is the case, then we must have
(mτY)f=mτX
and hence Em is a well-defined functor. Since m is monic,the converse is also true,and so Em is full.
Now suppose C has pullbacks along monomorphisms; we need to show that Em has a right adjoint Um:C/TC/S . Given an object (X,τX) in C/T ,we define Um(X,τX) to be (X,τX) in the following pullback: which exists since m is a monomorphism. Now let f:XY be a morphism of C/T . We define Um(f) to be f in the following diagram,which exists and is unique by pullback:
The natural transformations η(X,τX)=1X and ϵ(X,τX)=ιX witness that Um is right adjoint to Em ,and that UmEm=1C/S .
Remark 3.3.3. Note that it is the case that,for any graph T ,monomorphisms are exactly injective functions in both Graph and Graph /T . It follows that if m:ST is a graph monomorphism, Em and Um in the above theorem preserve and reflect monomorphisms.
We will sometimes, as in the next proposition, use the term pushout of monomorphisms; this refers to the pushout of a span of monomorphisms, as distinct from a pushout along a monomorphism where only one arrow in the span needs to be monic.
Proposition 3.3.4. Let S and T be graphs and m:ST a monomorphism. Then the functors Em:Graph/SGraph/T and Um:Graph/TGraph/S from theorem 3.3.2 preserve pushouts of monomorphisms.
Proof. All left adjoint functors preserve pushouts,and so Em does in particular.
Consider the following pushout of monomorphisms in Graph/T:
By the Set-based construction of Graph,we know that the above is a pushout if and only if D is covered by im(b) and im(c) and the intersection of those images is exactly the image of ba1=ca2 (note that this is only true because all the arrows in the diagram are monomorphisms).
We know that the following diagram commutes and consists of monomorphisms in C/S :
Recall the construction of,for example,the map Um(b) :
It suffices to show that,for each xUm(D),xim(Um(b)) if and only if ιD(x)im(b) and similarly for the other morphisms of the pushout. The argument is the same for each morphism, so we will only treat b . We can see from the left square of the diagram that if xim(Um(b)) ,then ιD(x)im(b)
For the converse,suppose ιD(x)im(b) ,and let y be its (unique) preimage under b . Now, τD(ιD(x))im(m) ,by the pullback square defining Um(D) . So then τB(y)im(m) ,since τDb= τB . So yim(ιB) by the pullback defining Um(B) and its preimage must map to x under Um(b) . Hence xim(Um(b)) .

3.3.1 String Graphs

Arbitrary graphs, however, are too general for our purposes. They have no concept of inputs or outputs, and so there is no clear way to represent a morphism. We therefore make use of string graphs, introduced as open graphs in [10] and further refined in [23]. These separate vertices into two kinds: node-vertices and wire-vertices. One way of viewing these is that, in translating the diagrams we saw in chapter 2 into string graphs, node-vertices correspond to the nodes of those diagrams, while wire-vertices "hold the wires in place". For example, the diagram
(S.)
could be represented as
R
where the larger white circle is a node-vertex and the smaller black ones are wire-vertices.
Just as terms were defined relative to a signature, we will define string graphs relative to a compressed monoidal signature. We will use a typegraph, so that the type of each node-vertex indicates which morphism symbol it represents, and the type of each wire-vertex indicates which object symbol it represents.
The following is adapted from the definition of a derived typegraph ([23], pp 88).
Definition 3.3.5. Given a compressed monoidal signature T=(O,M,dom,cod) ,the derived compressed typegraph GT has vertices O+M ,a self-loop mid X for every XO and,for every fM , - an edge inf,ia from X to f ,where (X,a)=dom(f)[i] ,for each index i of the list dom(f) ,and - an edge out f,ia from f to X ,where (X,a)=cod(f)[i] ,for each index i of the list cod(f) .
Example 3.3.6. Recall the compressed monoidal signature from example 3.2.5 .
f:[A][A,A]
g:[A,B][A]
The derived compressed typegraph would then be
The typegraph for the (spider) Z/X calculus (section 2.2) is very simple:
Let T=(O,M,dom,cod) be a compressed monoidal signature. Then for a graph (G,τ) in Graph /GT and a vertex v in G ,if τ(v) is in O ,we call v a wire-vertex. Otherwise, τ(v) must be in M ,and we call v a node-vertex. We denote the set of wire-vertices W(G) and the set of node-vertices N(G) . If v is a node-vertex and e is an edge incident to v ,we call e variable-arity if τ(e) is -tagged (eg: inf,1 ) and fixed-arity if it is -tagged (eg: ing,1 ). The fixed edge neighbourhood N(v) of a node-vertex v is the set of edges in the edge neighbourhood of v that are fixed-arity.
In general, we will depict wire-vertices as small black dots.
Definition 3.3.7 (Arity-matching). A map f between GT -typed graphs G and H is arity-matching if for every vN(G) ,the restriction of f to the fixed edge neighbourhood of v is a bijection onto the fixed edge neighbourhood of f(v) .
Note that,by considering GT as the typed graph (GT,1GT) ,we can view typing morphisms as morphisms of Graph/GT ,and hence apply the above terminology of arity-matching to typing morphisms.
The following is adapted from the definition of a string graph in [23], pp 89; it is equivalent to the original definition if GT has no variable-arity edges.
Definition 3.3.8 (String Graph). A GT -typed graph (G,τG)Graph/GT is a string graph if τG is arity-matching and each wire-vertex in G has at most one incoming edge and at most one outgoing edge. The category SGraphT is the full subcategory of Graph/GT whose objects are string graphs.
We refer to a wire-vertex of a string graph G with no incoming edges as an input,and write the set of all inputs In(G) . Similarly,a wire-vertex with no outgoing edges is called an output,and the set of all such vertices is written Out(G) . The inputs and outputs together form the boundary of the graph,written Bound(G) .
We will only consider finite string graphs and finite graphs in SGraphT ,since we are only interested in graphs that are tractable for computers.
Lemma 3.3.9. If f:GH is a morphism in SGraph and v is a vertex in G that maps to an input (respectively output) of H under f ,then v must be an input (respectively output) of G .
Proof. Suppose e is an edge of G such that tG(e)=v . Then tH(f(e)) must be f(v) ,and so f(v) cannot be an input unless v is. The output case is symmetric.
It is worth noting that not every subgraph of a string graph (in Graph/GT ) is a string graph. In particular,if G is a string graph, n is a node-vertex in G and e is a fixed-arity edge incident to n , a subgraph of G that contains n but not e will fail to satisfy the arity-matching requirement of the typing morphism. However, the intersection and union of two string graphs are still string graphs.
Proposition 3.3.10. Let G and H ,both string graphs,be subgraphs of the string graph K . Then GH and GH are both string graphs.
Proof. Any subgraph of a string graph satisfies the requirements about wire-vertices, so we only have to consider whether the typing morphisms are arity-matching. What is more, the typing morphism of any subgraph of a string graph must be injective at the fixed-arity neighbourhood of any of its node-vertices; we just need to consider sujectivity.
Let n be a node-vertex in GH and let τGHn be the restriction of τGH to the fixed-arity neighbourhood of n . Let e be a fixed-arity edge adjacent to τGH(n) in the typegraph. Then both τGn and τHn must have e in their images,and hence so much τGHn . Thus τGHn is surjective onto the fixed-arity neighbourhood of the typegraph,and so τGH is arity-preserving.
The argument for GH is similar.
Remark 3.3.11. The construction of the typegraph GT means that there can be no edges between node-vertices; any connection between node-vertices is mediated by wire-vertices. Since wire-vertices in string graphs have at most one input and one output,every string graph G is simple,in the sense that for any two vertices v,w of G ,there is at most one edge between v and w in each direction.
Proposition 3.3.12. Every morphism in SGraphT is arity-matching.
Proof. Let G and H be string graphs and f:GH a graph morphism. Consider vN(G) . Since τG=τHf ,we know that the restriction of these maps to N(v) is identical. But τG is arity-matching,and so its restriction to N(v) is a bijection,and hence the same is true of τHf . But that means that f restricted to N(v) must also be a bijection,as required.
The following is adapted from a similar proof in [23], pp 90. We can conclude from it that SGraphT is what Kissinger calls a partial adhesive category; we have chosen not to use this notion on the basis that it does not improve the clarity of the work.
Proposition 3.3.13. A morphism of SGraphT is monic if and only if it is injective.
Proof. Since this holds in Graph/GT ,any injective map in SGraphT must be monic in Graph/GT , and hence also monic in SGraphT .
Suppose we have a non-injective morphism f:GH in SGraphT . Then f must either map two or more edges in G to the same edge in H or map two or more vertices in G to the same vertex in H . In fact,since G and H are both simple, f must map two or more vertices vi in G to a single vertex v in H . Consider the subgraph K of H containing f(vi) . This must be the vertex,together with any incident fixed-arity edges (and the wire-vertices at the other end of those edges). Then for each vi ,we construct the string graph morphism gi that takes the single vertex in K to vi ,and the fixed-arity edges to the correct incident edges of vi (to make the typing morphisms commute). Now all the fgi are the same morphism,but the gi morphisms are distinct,so f is not monic.
For the rest of this chapter,we fix an arbitrary compressed monoidal signature T ,and objects and morphisms will be implicitly drawn from SGraphT unless otherwise stated.

Wires

It will sometimes be useful to have a different view of a string graph, where we treat each connected string of edges and wire-vertices as a single unit. As the name wire-vertex suggests, we will refer to these as wires.
We use a different definition of wires (and wire homeomorphisms) to [23]; our definition has several advantages, notably allowing for proposition 3.3.17 and being able to refer to explicit wire homeomorphisms. However, despite the different approach, the two definitions are morally equivalent.
Definition 3.3.14 (Wire). A wire path of a string graph G is a path in G containing at least one edge, whose internal vertices are all wire-vertices, and which is not contained in a longer path of this kind.
A closed wire of G is a pair (WV,WE) such that there is a wire path W of G where WE is the set of edges in W and WV is the set of vertices of W .
An open wire of G is a pair (WV,WE) such that there is a wire path W of G where WE is the set of edges in W and WV is the set of internal vertices of W ,plus the start/end vertex if W is a cycle.
Wires (G) is the set of all open wires of a string graph G .
Note that an isolated wire-vertex (with no incident edges) is not a wire path.
Proposition 3.3.15. Let G be a string graph. Then two distinct wire paths either describe the same cycle or overlap only on their start and end vertices.
Proof. The maximality requirement of wire paths means that, except in the case of cycles, the start or end vertex of one path cannot be an internal vertex of another. So distinct paths with a shared component must diverge at some point. However, the requirements of a string graph mean this cannot happen at a wire-vertex, and so can only happen at the start or end vertex. Thus either the paths are identical (or, at least, describe the same cycle) or are distinct everywhere except the start and end vertices.
This means there is a one-to-one correspondence between open and closed wires. In most cases, it will not matter whether we are referring to an open or a closed wire, and so we will simply use the term wire. It also means that each wire path gives rise to only one closed wire and one open wire, and only wire paths that describe the same cycle produce the same wire.
Proposition 3.3.16. The wire paths,and hence wires,of a string graph G can be sorted into the following disjoint kinds, based on their start and end vertices:
  • circles, where the start and end vertices are the same;
  • interior wires, where the start and end vertices are both node-vertices;
  • bare wires,where the start and end vertices are distinct wire-vertices,the start in In(G) and the end in Out(G) ;
  • input wires,where the start vertex is a wire-vertex in In(G) and the end vertex is a node-vertex; and
  • output wires, where the start vertex is a node-vertex and the end vertex is a wire-vertex in Out(G) .
Additionally, all the wire-vertices of a wire path have the same type, and this is called the type of the wire path (and of its derived open and closed wires).
Proof. The main thing we need to note for the categorisation is that if the path is not a cycle (and hence not a circle), the maximality requirement on a wire path requires the start or end vertex to be in Bound (G) if it is a wire-vertex,since otherwise it could be an internal vertex of a longer wire path.
The second part is a consequence of the construction of GT ,which disallows edges between wire-vertices of distinct types.
For wires other than circles, we call the start vertex of the path it is derived from the source of the wire, and the end vertex its target. Closed wires include their source and target, while open wires do not.

Proposition 3.3.17. Let G be a string graph. Then N(G) ,Bound (G) and the elements of Wires(G) cover G exactly (with no overlap).

Proof. Suppose v is a wire-vertex of G not in Bound (G) . Then it must have both an incoming and an outgoing edge. These, together with their respective source and target, form a path whose internal vertices are wire-vertices. This must either be a wire path of G or else be part of a longer wire path,and hence v is part of an open wire of G . Similarly,any edge of G trivially forms a path whose internal vertices are wire-vertices,and is therefore contained in an open wire of G . So these components cover G .
N(G) and Bound(G) cannot overlap,due to the typegraph. Similarly,open wires contain no node-vertices,and so cannot overlap N(G) . Any vertex in an open wire is an internal vertex of a path,and so cannot be in Bound (G) . Finally,proposition 3.3.15 gives us that no two open wires intersect.
Wire homeomorphisms provide a way to map between graphs that are equivalent under this view.
Definition 3.3.18 (Wire Homeomorphism). A wire homeomorphism f:GH between two string graphs G and H consists of three bijective type-preserving functions
-fN:N(G)N(H)
-fB:Bound(G)Bound(H)
-fW:Wires(G)Wires(H)
such that for each wire w in Wires(G) with a source v in N(G) (resp. Bound (G) ),the source of fW(w) in H is fN(v) (resp. fB(v) ),and similarly for targets of wires.
If there is a wire homeomorphism from G to H ,then G and H are said to be wire homeomorphic.

3.4 Valuation

In order for reasoning using string graphs to be useful, we need some way to interpret them. Node-vertices are intended to correspond to morphisms of a category, wire-vertices to objects of the category and edges to some concept of "information flow". The inputs of a graph naturally correspond in some way to the domain of the morphism represented by the graph, and the outputs to the codomain.
The construction of the value of a graph is essentially the same as the one Kissinger uses when he constructs a free traced SMC and a free compact closed category using string graphs ([23], pp 96-99, 104-112). We bring the notion of the value of a graph to the fore here, however, as we are more concerned with that than with free categories.
Our approach will be to fix an order on the inputs and outputs of a graph, using framed cospans, and then to break down the graph into elementary subgraphs that we can use a valuation (definition 3.2.7) to assign values (morphisms) to. For example, the graph(3.1)
will be broken down into
which will be assigned morphisms,say f,g,1A and 1B respectively. We then take the tensor product of these morphisms
and use the trace, in the form of a contraction, to link the morphisms together in the manner indicated by the connections of the original string graph
Swap maps and dual maps are then applied as necessary to get the inputs and outputs in the right order.

3.4.1 Framed String Graphs

Order is important. In a monoidal category, the morphisms
f:ABCD and g:BADC
cannot be the same, although in a symmetric monoidal category, it is possible that
f=γD,CgγA,B
In particular,consider the swap and identity morphisms for AB in a symmetric monoidal category
γA,B:ABBA and 1AB:ABAB
This would naturally be represented in string graph form as
However, these are the same graph (or, at least, isomorphic), and so there is no sensible way to assign one the value of γA,B and the other 1AB . In a compact closed category,we have a similar issue with the morphisms
dA:AAI,1A:AA and eA:IAA
whose graph representations should look like
To deal with this, we use framed cospans 23.
Definition 3.4.1 (Framed Cospan). A string graph frame is a triple (X,<,sgn) where X is a string graph consisting only of isolated wire-vertices, < is a total order on VX ,the vertices of X ,and sgn:VX{+,} is the signing map.
A cospan XdGcY is called a framed cospan if
  1. X and Y are string graph frames
  1. G contains no isolated wire-vertices
  1. the induced map [d,c]:X+YG restricts to an isomorphism
[d,c]:X+YBound(G)
  1. for every vVX,d(v)In(G)sgn(v)=+
  1. for every vVY,c(v)Out(G)sgn(v)=+
The frames can be seen as "holding the boundary in place". The signing map indicates inputs that appear in the codomain of the span, and outputs that appear in the domain, with a - . These correspond to dual objects in compact closed categories. A framed cospan where every vertex in both frames is + is called positive.
Given a string graph G ,we will often use G^ to refer to some fixed framing of it (ie: a framed cospan where the shared domain is G ). The particular framing,if it is relevant,will be given by the context.
The composition H^G^ of two framed cospans
XdGcYYdHcZ
is formed by the pushout
where the resulting cospan is
Xp1dHGp2cZ
Remark 3.4.2. We remarked earlier that proposition 3.3.12 means that SGraphT is what Kissinger calls a partial adhesive category in [23]. This, and the value construction above, form the necessary components for applying his proofs ([23], pp 104-112) that that classes of framed cospans up to wire homeomorphism form a compact closed category, and homeomorphism classes of positive framed cospans form a symmetric traced category, to our extended version of string graphs.

3.4.2 Indexings and Contractions

Before we define the value of a graph, we will need some notation. We fix a traced symmetric monoidal category C .
Definition 3.4.3 (Indexing). Let O be a (small) set of objects of C . For an object X of C ,an X -indexing is an indexed tensor product of the form
Xi1Xin
that is isomorphic to X . We call a morphism f:XY indexed when we have fixed an X -indexing and a Y -indexing.
For an X -indexing as above,we define the map shunt X:k to be the (unique) isomorphism constructed from the identity and swap maps of C that moves the Xk element of the X -indexing to the end and leaves all others the same, as in the following diagram:
Definition 3.4.4 (Contraction). Given an indexed map f:Xi1XimYj1Yjn ,where Xk=Yl ,the contraction of f from k to l,Ckl(f) ,is the morphism
TrXk(shuntY:lfshuntX:k1)
A contraction of an indexed morphism yields another indexed morphism. We can therefore apply multiple contractions to the same morphism, and these contractions commute:
Proposition 3.4.5 (Kissinger). For an indexed morphism f and distinct indices i,i,j and j ,
Cij(Cij(f))=Cij(Cij(f))
Proposition 3.4.6. Given X - and Y -indexings Xi1Xim and Yj1Yjn ,and morphisms
f:Xi1XikYj1Yjl
and
g:Xik+1XimYjl+1Yjn
if p=ia for some a>k and q=jb for some b>l ,then
Cpq(fg)=fCpq(g)
Proof. This follows from the definition and the laws of traces.

3.4.3 Value

Let V be a symmetric traced category,and let v be an expansion-order invariant valuation of T over V . For a framed cospan G^=XGY of SGraphT ,we define the value of G^ under v in the following manner.
The elementary subgraphs of G are those subgraphs that consist of one of the following:
  • a single node-vertex together with its incident edges and adjacent wire-vertices
  • an edge between wire-vertices, together with those wire-vertices (which may be the same vertex)
0 or 0
  • a wire-vertex that has no incident edges in G
Note that these are all valid string graphs. The definition of a string graph (and, in particular, the restriction on incident edges of wire-vertices) means that:
  • G is covered by its elementary subgraphs,
  • no node-vertex or edge appears in more than one elementary subgraph,
  • wire-vertices appear in at most two elementary subgraphs, and
  • any wire-vertex that does appear in two elementary subgraphs is an input in one and an output in the other.
Example 3.4.7. The string graph(3.2)
has the following four elementary subgraphs:
We then assign a value to each of these subgraphs, as well as a wire-vertex-based indexing for the domain and codomain of that value.
For an elementary subgraph H of G with a node-vertex n ,let f=τH(n) ,and for each incoming edge inf,ia of f in GT ,let d(i) be the size of the preimage of the edge under τH (ie: the number of edges adjacent to n that map to it),and define c(j) similarly for each outgoing edge out f,ja . Then these are arity counts for f ,since τG ,and hence τH ,is arity-matching. The value of H is then vmf(d,c) .
Consider A ,the domain of vmf(d,c) ,and let D(H) be the set of wire-vertices of H that are the source of an incoming edge of n . If D(H) is empty, A=I . Otherwise,for each input w of H with adjacent edge e ,let λ(w)=i ,where τH(e)=inf,ia . We can then choose a total order for D(H) such that λ is non-decreasing,and this ordered set provides an A -indexing with the property that if dom(f)=[α1,,αm] ,then Aw=αλ(w) . We can construct a similar indexing for the codomain of vmf(d,c) using C(H) ,the set of targets of edges whose source is n (unless this is empty).
If H is instead an edge e connecting two wire-vertices,we assign the value 1vo(Z):vo(Z)vo(Z) , where Z is the image of s(e) (and hence also of t(e) ). We set D(H)={s(e)} and C(H)={t(e)} (note that these may be the same). If H is an isolated wire-vertex w of type Z ,we similarly assign the value 1vo(Z) and set D(H)=C(H)={w} .
We then let g0 be the tensor product of the values of each elementary subgraph of G . A diagrammatic representation of this morphism for the graph (3.2) is
Let W1(G) be the union of D(H) and W2(G) the union of C(H) for the elementary subgraphs H of G . The total orders we placed on the inputs of each elementary subgraph of G ,together with the order of the tensor product g0 ,gives us an order on W1(G) ,and (providing W1(G) is not empty) this gives rise to a W1(G) -based indexing of the domain of g0 that agrees with the indexings we constructed for the elementary subgraphs; the same can be done for the codomain of g0 using W2(G) .
Now we order the wire-vertices w1,,wm of G that appear in both W1(G) and W2(G) ,but are not isolated wire-vertices in G ,and for 1im let
gi=Cwi,wi(gi1)
For the previous example, this would result in
Note that In(G)Out(G)=W1(G)W2(G) and,conversely, Out(G)In(G)=W2(G)W1(G) . This means that,given that the isolated wire-vertices of G are the only vertices to be both inputs and outputs of G ,the remaining indices in the indexing of the domain of gm are exactly the inputs of G ,and those in the indexing of the codomain are its outputs.
This means we can simply precompose and postcompose gm with the necessary swap maps to re-order the indexings of its domain and codomain to agree with the orderings of the frames of G^ . We call the resulting morphism v(G^) ,the value of G^ .
This final reordering means that the choice of order of elementary subgraphs when constructing g0 will not affect the value of G^ . The fact that contractions commute means that the choice of order of wire-vertices in G when constructing the maps g1,,gm does not affect the value of G^ . Finally,since the valuation v is expansion-order invariant,the choice of indexing for the domains and codomains of the elementary subgraphs of G does not affect the value of G^ .
In a compact closed category, a combination of swap maps and the maps associated with dual objects can be used to produce v(G^) from gm .
Note that the domain and codomain of v(G^) depend only on the frames,not on G . Note also that the frames only affect the final part of the construction, and so the values of two different framed cospans with the same internal string graph are the same up to pre- and postcomposition with swap maps if both are positive, and swap maps and dual object maps otherwise.
We will assume all valuations are expansion-order invariant from now on.
Proposition 3.4.8. Suppose G^=XgxGgyY and H^=ZhzHhwW are framings and f:GH is a wire homeomorphism such that the following diagram commutes
where the triangles on the left and right are taken from the definition of a cospan frame, and the top and bottom morphisms are order- and sign-preserving. Then,for every valuation v ,
v(G^)=v(H^)
Proof. We start by noting that the diagram above means we can identify X with Z,Y with W and Bound(G) with Bound(H) in a consistent manner.
Now we make the observation that if G and H are wire-homeomorphic,then there is a third graph K that is wire-homeomorphic to both where no two wire-vertices are adjacent to each other. What is more, K can be reached from both G and H by a (finite) series of 0 or more wire contractions, where an edge e between two distinct wire-vertices is removed,and s(e) and t(e) are identified. Thus we just have to show that the value of a framed cospan is stable under wire contraction, and the result follows by transitivity.
So let e be an edge of G whose source and target are distinct wire-vertices. Then e (together with its source and target) is an elementary subgraph of G . If s(e) is an input of G and t(e) is an output,contracting e will make no difference to the value of G^ ,as we will simply be replacing one elementary subgraph with another that has the same value, and there are no contractions in either case.
So suppose s(e) is not an input of G . Then s(e)W2(G) ,and there is a contraction Cs(e)s(e) . We can choose to place the elementary subgraph containing e last and apply the contraction on its source first. Cs(e)s(e)(g0) will then have the form (where we only display the last swap of the contraction)
where g0 is the tensor product of the elementary subgraphs of the contracted form of G together with all but one swap from the contraction of s(e) . Then we have
Cs(e)s(e)(g0)=g0
by the trace axioms. The extra swaps are irrelevant to the value of the contracted form of G^ as they are either absorbed into Ct(e)t(e) if t(e) is not an output,or are corrected at the end to account for the frame ordering.
The case where t(e) is not an output of G is symmetric. So the value of G remains the same after contracting e ,as required,and hence we have the required result.

3.5 Graph Equations

Our aim is to be able to mechanise equational reasoning for diagrams using string graphs. However, we first need to establish what we even mean by a "graph equation", and develop an equational logic for this concept.
Recall that in the equational logic for terms,there are rules that state that is closed under contexts and substitutions. We can view substitutions as a sort of internal context. For example, if we say
f(x)g(x)
we mean that we can replace f with g (or vice versa) regardless of what is either inside or surrounding that symbol. This approach is well-suited to the tree-like structure of terms, where there is a single external context and variables provide an easy way of labelling internal contexts, but does not work so well for graphs, which have only an external context, but may have multiple points of interaction with that context.
Declaring that two morphisms are equal only makes sense if both morphisms have the same type. Given our intended interpretation of the string graphs, this means that they need the same inputs and outputs (respecting types). But that is not enough; consider the associativity law for multiplication. For terms, we would have something like
m(m(x,y),z)m(x,m(y,z))
while with string graphs we would want something like
Visually, the meaning of this is clear, but we need some way to encode the correspondance between inputs; after all, one way of correlating the inputs would result in a law that was simply a consequence of commutativity:
We encode the correspondance of inputs and outputs using a span of graph morphisms whose images are the boundaries of the two graphs. We place some extra coherence requirements on the span to ensure that inputs are linked to inputs and outputs to outputs.
Definition 3.5.1 (String Graph Equation; [23],pp 93). A string graph equation Li1,i2R is a span Li1Ii2R where:
  • L and R contain no isolated wire-vertices;
  • In(L)In(R) and Out(L)Out(R) ;
  • Bound(L)IBound(R) ; and
  • the following diagram commutes,where j1,j2,k1 and k2 are the coproduct inclusions into the boundary composed with the above isomorphisms:
We can assemble similar laws to those we had in the term-based equational logic. Axiom, reflexivity and symmetry are straightforward:
 (REFL) EGbG,bGG (SYM) EGi,jHEHj,iG
where bG:Bound(G)G is the obvious inclusion of the boundary of G into G . Transitivity requires a bit more work to express. If we have the graph equations
GiIjH
and
HkJlK
then the constraints on graph equations mean that k1j is both well-defined and an isomorphism IJ . If we take p:=i and q:=lk1j ,we can express transitivity as
(TRANS)EGi,jHEHk,lKEGp,qK
For this to reflect intuitive equational reasoning, though, we need to be able to apply equations in the context of larger graphs. Given graph equations
GiIjH
and
GiIjH
such that there are monomorphisms making the following diagram commute, and the squares in it pushouts,
then we have the following rule
(LEIBNIZ)EGi,jHEGi,jH
We actually need one more rule, to account for wire homeomorphisms. Given graph equations
GiIjH
and
GiIjH
we say they are wire homeomorphic if there are wire homeomorphisms g:GG and h:HH such that(3.3)where the isomorphisms are those induced by i,j,i and j (see definition 3.5.1). Given two such wire homeomorphic equations, we have the following rule
(HOMEO)EGi,jHEGi,jH
We should note here that multiple stacked applications of the LEIBNIZ rule can be condensed into a single application.
Proposition 3.5.2. Suppose we have the proof tree fragment
Then
 LEIBNIZ EGi,jHEGi,jH
is a valid proof tree fragment.
Proof. We must have the following commuting diagram
We just need to find a string graph D and suitable monomorphisms to make(3.4)
commute. We will only demonstrate how to construct the left part of the diagram, as the right side can be constructed in the same manner. First of all, D and its inclusion into G are formed by
pushout:
What is more, because the left square and outer squares are both pushouts, the right square must also be a pushout.
Now the left square of (3.4) can easily be seen to commute:
What is more, we have just established that the bottom square is a pushout, so the outer square must also be a pushout.
The triangle between I,D and G follows easily:

3.5.1 Soundness

We want to make sure these rules are sound with respect to the valuation we described in section 3.4. In other words, if the assumptions of one of the preceding rules holds under a particular valuation, then the conclusion must hold under the same valuation.
However, the rules above deal with string graph equations, and valuations apply to framed cospans. We need to introduce frames to both sides of a string graph equation in a way that is compatible with the span that forms the equation.
Definition 3.5.3. A framing of a string graph equation Li1,i2R is a pair of framed cospans XaLbY and XcRdY such that there are morphisms j1 and j2 forming the coproduct (ie: disjoint union) Xj1Ij2Y and making the following diagram commute:
Note that it is always possible to frame a string graph equation in the following way: let X be a subgraph of I ,and Y its complement. Place an arbitrary ordering on X and Y ,and construct signing maps so that sgnX(x)=+ if and only if i1(x) (and hence also i2(x) ) is an input,and sgnY(y)=+ if and only if i1(y) (and hence also i2(y) ) is an output. X and Y are then frames. We set j1 and j2 to be the natural inclusions,and define a,b,c and d by the above diagram. XaLbY and XcRdY are then framed cospans,and so we have a framing of the string graph equation.
In addition,fixing a framed cospan for either L or R fixes a framing for the equation. This is because fixing a and b ,for example,fixes j1 and j2 (since i1 is monic).
We say that a string graph equation Li1,i2R holds under a valuation v if for all framings (L^,R^) (all positive framings if the valuation is not over a compact closed category) we have that v(L^)=v(R^) . In fact,this is the same as saying we have this for any framing.
Proposition 3.5.4. For any valuation v and any string graph equation Li1,i2R ,if (L1,R1) and (L2,R2) are framings of Li1,i2R (where both are positive unless v is over a compact closed category),then v(L1)=v(R1) if and only if v(L2)=v(R2) .
Proof. Consider the domains and codomains of v(L1) and v(L2) ,indexed by the vertices of their respective frames, X1,Y1,X2 and Y2 .
Using the same construction as for the value,we can find a tensor product of identities i and maps c and d composed of identities,swaps and dual maps such that
v(L1)=c(v(L2)i)d
and this construction depends only on the frames of the cospans, since these are what determine the domains and codomains of the values and their indexings. But this means that we also have
v(R1)=c(v(R2)i)d
since L1 and R1 have the same frames,and L2 and R2 also share their frames. Thus if v(L2)=v(R2) , then v(L1)=v(R1) .
The same argument works in reverse,giving us that if v(L1)=v(R1) ,then v(L2)=v(R2) .
Soundness of the reflexivity and symmetry axioms follows from the reflexivity and symmetry of = . For transitivity,we just need to note that,given a framing (G^,K^) of Gp,qK ,there is a framed cospan H^ such that (G^,H^) and (H^,K^) are framings of Hk,lK and Gi,jH respectively.
Proposition 3.5.5. The LEIBNIZ rule for string graphs is sound. In other words, if we have the following commuting diagram
where the top and bottom spans are string graph equations,a framing (G^,H^) of Gi1,i1H and framing (K^,L^) of Kj1,j2L ,then for all valuations v ,
v(G^)=v(H^)v(K^)=v(L^)
Proof. By proposition 3.5.4, it suffices to choose a specific framing for each equation, instead of showing it for all framings.
Since all the arrows in the above diagram are monic (and hence injective), we will consider them to be subgraph relations (so G is a subgraph of K by g ,and so on). For convenience,we will use D to refer to D less any isolated wire-vertices.
We start by noting that I consists only of isolated wire-vertices,but G and K have no isolated wire-vertices. This means that,since K is a pushout of D and G from I ,each elementary subgraph of K must be an elementary subgraph of exactly one of D or G . Similarly, W1(K) (defined in section 3.4.3) is the disjoint union of W1(G) and W1(D) ,and likewise for W2(K) . The same results hold for L .
It then suffices to show that,when calculating the value of a framed cospan K^ of K ,we can choose framings (G^,H^) and (K^,L^) for the equations such that v(K^) is of the form
Canan(Ca1a1(d0v(G^)))
and v(L^) is
Canan(Ca1a1(d0v(H^)))
for some indexed morphism d0 . The result then follows immediately.
We choose an order for the elementary subgraphs of D (none of which are isolated wire-vertices), and an order for the variable-arity edges of those subgraphs. Tensoring the elementary subgraphs together in order gives us d0 ,which can be indexed by W1(D) and W2(D) ,appropriately ordered. We do the same for G and H to get g0 and h0 ,indexed similarly.
Now k0=d0g0 and l0=d0h0 are valid choices for the same values for K and L ,and we can order W1(K) using the order of W1(D) followed by the order of W1(G) ,and similarly for W2(K) , W1(L) and W2(L) . These can then be used to index k0 and l0 ,and these indexings agree with the indexings for d0,g0 and h0 .
Next,we arbitrarily order W1(G)W2(G) as b1,,bp and W1(H)W2(H) as c1,,cq . We apply the contractions Cbibi in order to k0 and Ccjcj to h0 to get kp and hq respectively. At this point, we note that, by proposition 3.4.6 ,
kp=d0Cbpbp(Cb1b1(g0))=d0gp
and similarly lq=d0hq . But if we choose the framing (G^,H^) so that the ordering of the frames matches the ordering of W1(G) and W2(G) ,we have that v(G^)=gp . To get v(H^) ,we may need to pre- and post-compose with swap maps to get an order that agrees with the frames. Call these s1 and s2 . Then v(H^)=s2hqs1 .
If we order (W1(K)W2(K))(W1(G)W2(G)) as a1,,an ,a similarly suitable choice of the framing (K^,L^) gives us
v(K^)=Canan(Ca1a1(d0v(G^)))
It remains to show that
v(L^)=Canan(Ca1a1(d0(s2hqs1)))
We need to consider the decomposition of s1 and s2 into their individual swap operations. If any given swap operates on an index that is then contracted (ie: one of the ai ),it can be subsumed into that contraction,due to the way contractions are defined. So we can construct reordering maps s1 and s2 that only operate on inputs and outputs (respectively) of L such that
Canan(Ca1a1(d0(s2hqs1)))=Canan(Ca1a1(d0(s2hqs1)))
But this is the same as
(1s2)Canan(Ca1a1(d0hq))(1s1)
We will refer to this (indexed) morphism as λ:AB .
We need to show that indexing of this morphism agrees with the order on the frames of L^= XLY . We will just treat the X frame,as the Y frame is symmetric. Note that we have the following commuting diagram,by the definition of a framing,which allows us to consider X a subgraph of D .
We split X ,which consists of the inputs of K (and therefore of L ) into two parts: X1 are those vertices that are inputs of D ,and X2 are the inputs of G (and hence of H ). Note that we can consider X1 a subgraph of D and X2 a subgraph of I .
Suppose a<bX . Then either both are in X1 ,both are in X2 or aX1 and bX2 . In the latter case,we know that a appears before b in the indexing of the domain of λ due to the construction of λ . Suppose both are in X1 . Then we know that Aa appears before Ab in the indexing of d0 ,because that is how we chose the ordering on X . Otherwise,both are in X2 . We know that Aa appears before Ab in the indexing of g0 ,and hence in the indexing of gp . If the same is true of the indexing of hq ,it must be the case that s1 ,and hence s1 ,does not swap the order of Aa and Ab ,and so Aa appears before Ab in the indexing of λ . Otherwise,if Ab is before Aa in the indexing of hq,s1 (and hence s1 ) must swap Aa with Ab ,and so we still have that Aa is before Ab in the indexing of λ .
Sov(L^)=λ,as required.
Proposition 3.5.6. The HOMEO rule for string graphs is sound. In other words, given wire-homeomorphic string graph equations Gi,jH and Gi,jH with respective framings (G^,H^) and (G^,H^) ,
v(G^)=v(H^)v(G^)=v(H^)
Proof. The precondition on the wire homeomorphisms allows us to construct framings of the equation that are consistent with each other in the manner required by proposition 3.4.8. From that proposition, we get
v(G^)=v(G^) and v(H^)=v(H^)
and it follows by transitivity of = that
v(G^)=v(H^)v(G^)=v(H^)

3.6 Graph Rewriting

Graph rewriting has been around in some form since at least the 60s; it made an early appearance in graph grammars, a field that aimed to apply formal language theory to multidimensional objects rather than just linear strings, notably in [33] and [36].
In term rewriting, we replaced a subterm of a term with another term that we viewed as equivalent in some way. In a similar manner, graph rewriting (at least as far as this thesis is concerned) aims to replace a subgraph of a graph with another "equal" graph. There are several approaches to this problem,almost all of which involve a graph L to be searched for and removed from the target graph
G ,a graph R to replace it with and some embedding transformation E describing how to map from the connectivity of L with GL to edges between R and GL .
Algebraic graph rewriting systems express E using constructs from category theory,which provides a useful set of tools for reasoning about such systems. Using these systems allows us to make use of established work, such as proofs that independent rewrites (which operate on different parts of G ) can be applied in either order and acheive the same result [14].
There are two main approaches to algebraic graph rewriting: single-pushout (SPO) and double-pushout (DPO). DPO was the first algebraic graph rewriting system, introduced by Ehrig, Pfender and Schneider in [15]. A rewrite rule is represented as a span of graphs
LiIjR
and a rewrite from G to H is a pair of overlapping pushouts
The embedding transformation is described by i,j and I . We can think of I as being the interface of the rewrite rule,the part allowed to interact with the rest of G . This part is held in place when the rest of L is removed from G ,allowing the connectivity with GL to be maintained.
SPO, as presented by Löwe in [41], generalises DPO by using a single pushout
in the category of partial graph morphisms. This allows for rewrites that would be prohibited under DPO, such as deleting vertices in unknown contexts. For example the SPO rewrite
has no equivalent DPO rewrite, because of the edge between the grey and black vertices.
We will make use of DPO as our graph rewriting system, as we do not require (and, in fact, wish to avoid) the extra flexibility of SPO.
Similar to the term case, we direct a string graph equation (definition 3.5.1) to get a string graph rewrite rule. Given a string graph rewrite rule LiIjR ,a string graph rewrite is a pair of pushouts of monomorphisms in SGraphT(3.5)
(which should also be familiar from the rules of section 3.5).
Note that the inclusion of D into G must contain Bound(G) in its image. This is because any input or output of G in the image of m must map from an input or output of L ,and must therefore be in the image of i . The same is true of the inclusion of D into H . What is more,the constraints on i and j mean that the preimages of Bound(G) and Bound(H) under these inclusions coincide. The same is also true for In(G) and In(H) and for Out(G) and Out(H) . If we let I be the shared preimage of the boundaries of G and H ,then - providing G and H have no isolated wire-vertices - the span at the bottom of
is a string graph rewrite rule.
As the term "rewriting" suggests, what we actually want to do is start with the string graph rewrite rule Li,jR and G ,and find the remainder of the diagram. We start by finding a matching, a map m:LG (see (3.5)) such that i and m can be extended to a pushout; ie: they have a pushout complement.
Definition 3.6.1 (Pushout complement). A pushout complement for a pair of arrows
AfBgC
is an object B and a pair of arrows
AfBgC
such that
is a pushout.
The following result is due to Dixon and Kissinger [11], based on a similar result for adhesive categories in [27].
Proposition 3.6.2. If a pair of arrows (b,f) in SGraphT ,where b is monic,have a pushout complement, it is unique up to isomorphism.
Definition 3.6.3 (String graph matching). For a string graph G and a string graph rewrite rule LiIjR ,a monomorphism m:LG is called a string graph matching if IiLmG has a pushout complement.
We require a stronger form of arity-matching in order to guarantee pushout complements:
Definition 3.6.4. A map f between GT -typed graphs G and H is a local isomorphism if for every v N(G) ,the restriction of f to the edge neighbourhood of v is a bijection onto the edge neighbourhood of f(v) .
Proposition 3.6.5 (Kissinger). Let LR be a string graph rewrite rule. Then any monic local isomorphism m:LG is a string graph matching.
So if we find a monomorphism m:LG ,we can assemble the first pushout square of (3.5): since i and m are monic,we can view them as expressing the subgraph relation. Then D is obtained by removing from G everything in the image of m but not in the image of mi . But we still need to be able to form the second pushout.
Boundary coherence proves to be the right notion for determining when we can form pushouts in SGraphT .
Definition 3.6.6. A span of morphisms GgIhH in SGraphT is called boundary-coherent if:
  1. for all vIn(I) ,at least one of g(v) and h(v) is an input; and
  1. for all vOut(I) ,at least one of g(v) and h(v) is an output.
A single morphism f:GH is called boundary-coherent if the span HfGfH is.
Theorem 3.6.7 (Kissinger). A span of morphisms GgIhH in SGraphT has a pushout if and only if it is boundary-coherent.
Our definition of a string graph rewrite rule means that the boundary coherence of the maps in the left-hand pushout propagates to the maps on the right, meaning that if we can construct one of the pushouts in (3.5), we can always construct the other one.
Lemma 3.6.8. Let LiIjR be a string graph rewrite rule and f:IG be a string graph morphism. Then i and f as a span are boundary-coherent if and only if f and j are.
Proof. This follows directly from the fact that,for all vertices w in I,i(w) is an input (resp. output) of L if and only if j(w) is an input (resp. output) of R .
Corollary 3.6.9. Let LR be a string graph rewrite rule and m:LG a monic string graph local isomorphism. Then LR has an S -rewrite at m .
Constructing the pushout is easy: pushouts along monomorphisms in Graph (and its slice categories) are just graph unions (with an explicit intersection). Likewise, pushout complements from monomorphisms can be calculated using graph subtraction. The above results guarantee that we will get valid string graphs when we do so.
Example 3.6.10. The following string graph rewrite is an application of the string graph rewrite rule for the unit law in the Z/X calculus:

3.6.1 Equational Reasoning with Rewrites

Rewriting is typically done with respect to some set of rewrite rules S ,called a (graph) rewrite system. We say that a string graph G rewrites to a string graph H under the graph rewrite sytem S (or GSH ) if there is a string graph rewrite rule LRS and a string graph matching m:LG such that
is a string graph rewrite.
If we define
S={Gi,jHGi,jHE}
then S implements the LEIBNIZ and AXIOM rules of the previously-presented equational logic for string graphs. In particular, string graph rewriting implements a single application of Axiom followed by a single application of LEIBNIZ (which, by proposition 3.5.2 is equivalent to any proof tree containing just Axiom and LEIBNIZ axioms).
It then follows that S ,the reflexive,symmetric,transitive closure of S ,implements the previously presented equational logic with HOMEO omitted.

3.6.2 Matching up to Wire Homeomorphism

There is one more rule we need to account for in our mechanisation process: HOMEO. Ideally, we would like to do rewriting "up to wire homeomorphism".
Given a string graph rewrite rule LR and a graph G ,we say that G rewrites to H by LR up to wire homeomorphism if there are G,H and LR ,wire homeomorphic to G,H and LR respectively,such that G rewrites to H by LR .
We would like to find the set H of graphs H such that G rewrites to H by LR up to wire homeomorphism,quotiented out by wire homeomorphism (ie: so there are no two graphs in H wire homeomorphic to each other).
We can eliminate duplicate wire homeomorphic graphs as a last step by settling on some standard form (such as have at most one wire-vertex on each wire other than bare wires, where we must have two). However, this does not help to ensure we have found all possible matches without trying the (likely infinite number of) graphs wire homeomorphic to G . We demonstrate a technique for constraining the search space at the matching step by making a careful choice of G and LR .
Any monomorphism from L to G must necessarily map wires of L onto wires of G of the same type in the following manner:
  • A circle of L must map to a circle of G ,in which case nothing else can map to that same circle
  • An interior wire of L can only map to an interior wire of G ,and this must be the only thing mapping to the wire.
  • A bare wire of L can map to any wire of G ,and may not be the only thing to map to that wire
  • An input wire of L can map to either an input wire or an interior wire of G ; in both cases,it may not be the only thing mapping to that wire
  • Output wires are similar to input wires
Note that multiple bare wires can match the same wire simultaneously
as well as matching an interior wire that has already been matched by an input and/or an output wire
or an input wire that has been matched by an input wire or an output wire that has been matched by an output wire.
Let n be the number of bare wires in L . We choose L to be the (unique,up to isomorphism) graph that is wire homeomorphic to L such that
  • every circle has max(2n,1) wire-vertices on it
  • every interior wire has exactly 2n+2 wire-vertices on it
  • every bare wire has no wire-vertices other than the input and output
  • every input or output wire has no wire-vertices other than the input or output itself
We then choose G to be the (unique,up to isomorphism) graph that is wire homeomorphic to G such that
  • every circle has max(2n,1) wire-vertices on it
  • every interior wire has exactly 2n+2 wire-vertices on it
  • every bare wire has exactly 2n wire-vertices on it (including boundary vertices)
  • every input or output wire has exactly 2n+1 wire-vertices on it (including the boundary vertex)
We say that these graphs are normalised.
Any algorithm for finding graph monomorphisms (such as those in [40] or [2]) can then be used (together with a suitable filter) to find local isomorphisms from L to GBound(G) . Now consider an arbitrary wire w of G .
  • If w is a circle,it can be matched by any circle of the same type in L ,since circles in both graphs have the same number of wire-vertices. Alternatively,if n>0 ,it can be matched by any or all of the n bare wires of L .
  • If w is an interior wire,it can either be matched by one of the interior wires of L (which have the same number of wire-vertices) or it can be matched by any combination of an input wire (consuming a single wire-vertex at one end), an output wire (similarly) and any or all of the bare wires (on the remaining 2n wire-vertices).
  • If w is a bare wire,it can be matched by any or all of the n bare wires of L .
  • If w is an input wire,it can be matched by an input of L ,which will consume one of the 2n+1 wire-vertices; this will still allow any or all of the bare wires of L to match.
  • Finally,if w is an output wire,it can similarly be matched by an output of L and/or any or all of the bare wires of L .
Rewriting using all of the matches found in this way will produce a finite collection H of rewritten graphs. Contracting all the wires in these graphs so that there is only a single wire-vertex on each, except for bare wires which need two wire-vertices, and eliminating the duplicates will give us the set H we originally wanted.
Remark 3.6.11. The proliferation of wire-vertices and edges between them in L and G when L has bare wires means that this is not the most efficient way of doing matching up to wire homeomorphism. Quantomatic takes a slightly different approach,initially assuming n=0 and delaying matching bare wires from L until everything else has been matched; each bare wire is then matched against an edge of G ,which is replaced by two wire-vertices and three edges at this point. See section 7.2 for details.
Example 3.6.12. The graph
would be normalised to
if it were the graph L from the rule and to
if it were the target graph G .

Chapter 4

!-Graphs

String graph rewrite systems have a shortcoming in that they do not have a finite way of representing infinitary rewrite rules. In this chapter, we present !-graphs (pronounced "bang graphs"), an extension of string graphs, as a way of expressing certain infinite families of string graphs in a finite way. In the next chapter, we will use these to construct infinite families of string graph rewrite rules and use them to rewrite string graphs, both directly and by rewriting !-graphs.
Recall the spider laws of section 2.2 that arose from commutative Frobenius algebras (CFAs):(4.1)
In a single diagram, this describes an infinite family of equations. However, while its meaning may be clear to a human, we need a more precise encoding for a proof assistant to be able to handle equations like this. In [9], Dixon and Duncan briefly described a system of graph patterns to handle laws like this. However, they provided no mathematical foundation for these. Kissinger, Merry and Soloviev provided such a foundation in [26] (as pattern graphs), making the system more powerful in the process. This joint work with the author of this thesis, which contained no proofs, forms the basis of this chapter, although we use the term !-graphs instead of pattern graphs to avoid confusion when describing matching (where the two graphs are often called the pattern and target graphs).
!-graphs formalise the notion of repetition indicated by the ellipses and encode it in the graph itself. What will actually be encoded is a collection of labelled subgraphs called !-boxes. A !-graph can be instantiated into a string graph by removing ("killing") or duplicating ("copying") these subgraphs (including incoming and outgoing edges) some (finite) number of times. In this way, a !-graph can stand in the place of an infinite family of string graphs:
We can even express the bipartite graph from the generalised bialgebra law
by nesting !-boxes inside other !-boxes:
Section 4.4.1 goes into detail about the effect of nested and overlapping !-boxes.

4.1 Open Subgraphs

Note: when we refer to a subgraph of a string graph in this section,we mean a subgraph in SGraphT - ie: the subgraph is also a string graph.
It should be clear that we cannot allow !-boxes to be arbitrary subgraphs. Copying b1 in the following graph, for example, will lead to an invalid string graph, as there will be a wire vertex with multiple outputs:
Copying or killing a !-box must also not affect the fixed-arity edges of node-vertices, otherwise the arity-matching property of the typing morphism will be broken.
So we must restrict our !-boxes to those that can be copied. For string graphs, the correct notion is that of open subgraphs. Note that the definition here differs from, but is equivalent to, the one in [26] (pp 5).
Definition 4.1.1 (Open Subgraph). A subgraph O of a string graph G is said to be open if it is not adjacent to any wire-vertices or incident to any fixed-arity edges.
This is also related to boundary-coherence in SGraph:
Proposition 4.1.2. Let G be a string graph,and H a subgraph of G in SGraphT . Then H is open if and only if it has a complement GH (in SGraphT ),and the embedding of this complement into G is boundary-coherent.
Proof. Suppose (H,τH) is open in (G,τG) ,and consider (GH,τGH) ,which is a graph in Graph/GT . Let n be a node-vertex in GH ,and let τGHn be the restriction of τGH to the fixed edge neighbourhood of n ,and similarly for τGn . Since GH is a subgraph of G,τGH is a restriction of τG . So τGHn is a restriction of τGn ,and hence is injective and its image consists only of fixed-arity edges of the typegraph. Suppose it is not surjective,so there is some fixed-arity edge e incident to τGH(n) that is not in the image of τGH . Then the preimage of e under τG,e ,must not be in GH . Since n is in GH ,and GH is full in G ,the other end of e ,which we will call w ,must be in H . But then H is incident to a fixed-arity edge (namely e ),and hence is not open in G . So GH is a string graph,since (being a subgraph of G ) it must have at most one incoming and one outgoing edge on each wire-vertex.
For boundary-coherence of the embedding ι:GHG ,we need to show that any input of GH is also an input of G ,and likewise for outputs. But the only way an input w in GH could not be an input in G is if there is an edge e in G from some vertex v to w . Because e is not in GH ,neither can v be. So v must be in H ,and so H is incident to a wire-vertex (w) ,contradicting the openness of H . The argument for outputs is analagous,and so we have boundary-coherence as required.
Conversely,suppose (H,τH) is a (string) subgraph of (G,τG) ,and that its complement is also a string graph with a boundary-coherent embedding ι into G . Suppose H is adjacent to a wire-vertex w ,via an edge e . Then w is in GH ,but e is not. If w is the target of e,w must be an input of GH but not of G . Otherwise, w is the source of e and w is an output of GH but not of G . Either way, ι cannot be boundary-coherent. So there is no such w .
Now suppose H is incident to a fixed-arity edge e . Let v be the end of e that is not in H.v cannot be a wire-vertex,since we have already shown that H cannot be adjacent to a wire-vertex. So v is a node-vertex. Let e=τG(e) . Then e is in the fixed neighbourhood of τG(v) ,but is not in the image of τGH . So τGH is not arity-matching,contradicting the assumption that (GH,τGH) is a string graph. Thus there can be no such edge e ,and H is open in G .
The use of the term "open" brings with it the expectation that the property is preserved under unions and intersections (since we are dealing with finite graphs). The following proposition shows that this is, indeed, the case.
Proposition 4.1.3 ([26],pp 5). If O,OG are open subgraphs,and HG is an arbitrary subgraph,then OO and OO are open in G and HO is open in H .
Proof. Proposition 3.3.10 gives us that the graphs are all string graphs.
Suppose OO is adjacent to a wire-vertex. Then there is a wire-vertex w in G but not in OO adjacent to a vertex v in OO . If w is not in O ,we have a contradition for the openness of O . So w must be in O . Similarly, w must be in O . But then w is in OO ,which contradicts our assumption. So there can be no such w . Instead,suppose OO is incident to a fixed-arity edge e . Again, e must be in O ,since O cannot be incident to a fixed-arity edge,and must also be in O for the same reason,and hence is in OO ,and so not incident to it. So there is no such e and OO is open in G .
Suppose OO is adjacent to a wire-vertex. Then there is a wire-vertex w in G but not in OO adjacent to a vertex v in OO.v must either be in O or O ; WLOG assume it is in O . Then,since w is not in O,O is adjacent to a wire-vertex. But this cannot be the case,since O is open,so there can be no such w . Similarly,if there is a fixed-arity edge e incident to OO ,it must be incident to either O or O ,which cannot be the case. So there is no such e ,and OO is open in G .
Suppose there is a wire-vertex w in H but not in HO adjacent to a vertex v in HO . Then w is in G but not in O ,and v is in O ,and they are joined by an edge in G . So O is adjacent to a wire-vertex in G ,contradicting its openness in G ,so there is no such w . Suppose now that HO is incident to a fixed-arity edge e in H ,and let v be the vertex in HO it is incident to. Then v is in O ,and e is in G but not O ,and so O cannot be open in G ,which contradicts the assumption. So there can be no such e ,and HO is open in H .

4.2 The Category of !-Graphs

The ! -boxes are encoded into the graph itself as a new vertex type. These ! -vertices act as the labels for the ! -boxes,and the edges from the ! -vertices to other graph vertices indicate the ! -box contents. We therefore need to extend the derived typegraph of a monoidal signature T to include this new vertex.
Definition 4.2.1 (Derived Compressed !-typegraph). The derived compressed !-typegraph GT! of a compressed monoidal signature T has the same vertices as GT (see definition 3.3.5) together with a distinct vertex ! ,and the same edges as GT together with a self-loop p! on ! and,for each vertex v of GT ,an edge pv from ! to v .
Note that the definition of GT! ensures that there can be no edges from wire- or node-vertices to !-vertices.
The derived compressed !-typegraph of the compressed monoidal signature
f:[A][A,A]
g:[B,A][A]
would be
The wire-vertex and node-vertex terminology is inherited from string graphs. In addition, for a graph (G,τ:GGT!) in Graph/GT! ,we call any vertex v where τ(v)=! a ! -vertex,and denote the set of all ! -vertices in G as !(G) .
We alter the definition of an input slightly from the string-graph case, due to the new vertex type: a wire-vertex is an input if the only in-edges are from !-vertices.
For a ! -vertex b!(G) ,let B(b) be its associated ! -box. This is the full subgraph whose vertices are the set succ(b) of all of the successors of b . We also define the parent graph of a !-vertex B(b) as the full subgraph of predecessors,that is,the full subgraph generated by pred(b) . Note that the typegraph constrains B(b) to only contain ! -vertices (and edges between them).
As a notational convenience,when dealing with subgraphs of GT! -typed graphs where the inclusion map is implicit,we will use subscripts to identify which graph we are referring to. So if H is a subgraph of G and b is a ! -vertex in H,BH(b) will be its ! -box in H ,and BG(b) will be the ! -box of b when considered as a vertex of G .
Note that,for a given monoidal signature T,GT is a subgraph of GT! . Since Graph has pullbacks, theorem 3.3.2 gives us a full,coreflective embedding E:Graph/GTGraph/GT! ,whose right adjoint is the forgetful functor U:Graph/GT!Graph/GT that simply drops all ! -vertices.
Definition 4.2.2 (!-Graph and BGraphT ; [26],pp 5). A GT! -typed graph G is called a !-graph if:
  1. U(G) is a string graph;
  1. the full subgraph with vertices !(G) ,denoted β(G) ,is posetal;
  1. for all b!(G),U(B(b)) is an open subgraph of U(G) ; and
  1. for all b,b!(G) ,if bB(b) then B(b)B(b) .
BGraphT is the full subcategory of Graph/GT! whose objects are !-graphs.
Recall that a graph is posetal if it is simple (at most one edge between any two vertices) and, when considered as a relation,forms a partial order. Note in particular that this implies bB(b) (and B(b) ),by reflexivity. This partial order allows !-boxes to be nested inside each other,provided that the subgraph defined by a nested !-vertex is totally contained in the subgraph defined by its parent (condition 4).
As with string graphs, we only consider finite !-graphs in the sequel.
We introduce special notation for !-graphs. !-vertices are drawn as squares, but rather than drawing edges to all of the node-vertices and wire-vertices in B(b) ,we simply draw a box around it.
In this notation,we retain edges between distinct ! -vertices to indicate which ! -boxes are nested as opposed to simply overlapping. This distinction is important, as nested !-boxes are copied whenever their parent is copied.
We will prove a few useful results about !-graphs and about BGraphT . Firstly,we have a sufficient condition for a subgraph of a !-graph to be a !-graph.
Lemma 4.2.3. Let G be a !-graph and H a full subgraph of G such that U(H) is a string graph. Then H is a !-graph.
Proof. U(H) is a string graph by assumption.
Since H is full in G,β(H) must be a full subgraph of β(G) . But a full subgraph of a posetal graph is itself posetal,so β(H) is posetal.
Let b!(H) . Then U(BG(b)) is an open subgraph of U(G) ,and U(BH(b))=U(BG(b))U(H) , which is open in H by proposition 4.1.3
Let b,c!(H) ,with cBH(b) . Then we must have cBG(b) ,since G is a !-graph. So BG(c)BG(b) . Since H is full in G ,we know that BH(b)=BG(b)H and similarly for c . Then BG(c)HBG(b)H ,so BH(c)BH(b) .
So H is a !-graph,as required.
Corollary 4.2.4. Let G be a 1-graph,and H a subgraph of G such that U(H) is open in U(G) . Then GH is a !-graph.
It is also useful to know under what conditions a !-graph morphism is monic or (strongly) epic in BGraphT . These conditions turn out to be the same as for SGraphT .
Lemma 4.2.5. A morphism in BGraphT is monic iff it is injective.
Proof. Since this holds in Graph/GT! ,any injective map in BGraphT must be monic in Graph/GT! , and hence also monic in BGraphT .
Suppose we have a non-injective morphism f:GH in BGraphT . Then f must either map two or more edges in G to the same edge in H or map two or more vertices in G to the same vertex in H . In fact,since G and H are both simple, f must map two or more vertices vi in G to a single vertex v in H . Consider the smallest sub-l-graph K of H containing f(vi) . This is the vertex itself, plus a self-loop if it is a !-vertex or any fixed-arity edges (plus their terminating wire-vertices) if it is a node-vertex. Then for each vi ,we construct the !-graph morphism gi that takes the single vertex in K to vi (this will extend to any incident edges of the vertex in K in a unique way,dictated by the typing morphisms). Now all the fgi are the same morphism,but the gi morphisms are distinct, so f is not monic.
Lemma 4.2.6. Let f:GH be a ! -graph morphism. Then f[G] ,the image of f ,is a ! -graph.
Proof. First we note that f[G] is a subgraph of H ,and let ι:f[G]H be the inclusion. Then U(f[G]) is a subgraph of the string graph U(H) . It therefore satisfies the wire-vertex conditions for string graphs,and we only need check that τH restricts to an arity-matching morphism. But we know that f is arity-matching,and hence restricts to a bijection on the fixed-arity neighbourhood of every node-vertex v in G and its image in H ,and τG is also arity-matching,and τG and τHf commute. So τHf[G] must be arity-matching,and hence U(f[G]) must be a string graph.
β(f[G]) is a subgraph of β(H) . But then β(f[G]) is simple and anti-symmetric,since H is,and is reflexive and transitive,since G is,and hence is posetal.
Let b!(f[G]) . Then there is a b!(G) with ι(b)=f(b) . Now B(b)=B(f(b))f[G] ,which is open in f[G] by proposition 4.1.3.
Let b,c!(f[G]) ,with cB(b) . Then we must have ι(c)B(ι(b)) . So B(ι(c))B(ι(b)) . But then B(b)=B(ι(b))f[G] and similarly for c ,and B(ι(c))f[G]B(ι(b))f[G] ,so B(c)B(b) . So f[G] is a !-graph,as required.
Lemma 4.2.7. A morphism in BGraphT is a strong epimorphism iff it is surjective.
Proof. Since this holds in Graph/GT! ,any surjective map in BGraphT must be a strong epimorphism in Graph/GT! ,and hence a strong epimorphism in BGraphT .
Now suppose e:AB is a strong epimorphism. Let e:Ae[A] be the restriction of e to its image (which is also a !-graph by lemma 4.2.6) and let ι:e[A]B be the inclusion of the image of e in B . Then ι is monic,so there exists a map d making the following diagram commute:
But then ιd=1B ,so ι must be surjective and hence so is e .
Finally,it is worth noting how SGraphT and BGraphT are related.
Definition 4.2.8 (Concrete Graph). A !-graph with no !-vertices is called a concrete graph.
The full subcategory of BGraphT consisting of concrete graphs is,in fact,the image of SGraphT under the previously-mentioned embedding functor E . Concrete graphs and string graphs will therefore be considered interchangable.
Indeed,the restriction of E to SGraphT is a full,coreflective embedding,and its right adjoint is the restriction of U to BGraphT . As a result,we will also use E and U to refer to these restrictions; which is meant should be clear from context. We use to mean EU (and note that BGraphT is closed under ).
We can extend the β(G) notation of definition 4.2.2 to morphisms of Graph/GT! (and hence of BGraphT ) by making their operation be the obvious restrictions. More precisely,if G! is the subgraph of GT! consisting of only the !-vertex and its self-loop (with ιT being its inclusion map), we can view β as EιTUιT (in the terminology of theorem 3.3.2).

4.2.1 Wire Homeomorphisms

We will need to extend our notion of wire-homeomorphism to !-graphs.
A wire homeomorphism f:GH between two !-graphs G and H consists of four bijective type-preserving functions
-fN:N(G)N(H)
-f!:!(G)!(H)
-fB:Bound(G)Bound(H)
-fW:Wires(G)Wires(H)
such that
  • for each wire w in Wires(G) with a source v in N(G) (resp. Bound (G) ),the source of fW(w) in H is fN(v) (resp. fB(v) ),and similarly for targets of wires
  • for each b!(G) ,there is an edge in G from b to a vertex v in !(G) (resp. N(G) ,Bound (G) ) if and only if there is an edge in H from f!(b) to f!(v) (resp. fN(v),fB(v) )
  • for each b!(G) and each wire wWires(G) ,there is an edge in G from b to each vwV if and only if there is an edge in H from f!(b) to each v(fW(w))V
This is the same as the definition for string graphs, but with a map for !-boxes and some constraints to preserve !-box containment. This means that if f:GH is a wire-homeomorphism of !-graphs,discarding f! will give a wire-homeomorphism U(G)U(H) .

4.3 The !-Box Operations

We have already mentioned that ! -boxes are intended to be subgraphs that can be copied or deleted.
The precise set of operations allowed on a !-box are the following ([26], pp 6, although we omit MERGE from that list and revisit it in section 6.5 :
These are inspired by the rules for the "bang" operation from linear logic 16. In particular, COPY corresponds to contraction, DROP to dereliction and KILL to weakening.
Definitions 4.3.1 (!-Box Operations; [26],pp 6). For G a !-graph and b!(G) ,the three !-box operations are defined as follows:
  • COPYb(G) is defined by a pushout of inclusions in Graph/GT! :
(4.2)
-DROPb(G):=Gb
-KILLb(G):=GB(b)
Before we show that these operations preserve the property of being a !-graph, it will be useful to adapt the notion of boundary-coherence to !-graphs. The important thing is that, in addition to the restrictions on how the morphisms interact with the boundaries of the graphs, we also need to restrict how they interact with ! -box containment. Note that the definition of boundary- ! -coherence we give here is stronger than is actually needed for producing pushouts of !-graphs; this gives us a simpler definition and simpler proofs.
Definition 4.3.2. Let f:GH be a !-graph morphism. f is said to reflect !-box containment if whenever we have an edge e in H whose source is a !-vertex and whose target is in the image of f , e is also in the image of f .
A span of monomorphisms GgIhH in BGraphT is called boundary-!-coherent if the span formed from U(g) and U(h) is boundary-coherent and both g and h reflect !-box containment.
As in SGraphT ,a single morphism f:GH of string graphs is called boundary- ! -coherent if the span HfGfH is.
The main purpose of this definition is to provide us with a sufficient condition for a span to have a pushout in BGraphT .
Proposition 4.3.3. If a span of monomorphisms GgIhH in BGraphT is boundary-!-coherent, then it has a pushout in BGraphT .
Proof. Suppose g and h are boundary-!-coherent. Since they are monomorphisms,they have a pushout in Graph /GT! :(4.3)
It suffices to show that D is a !-graph.
The span formed by U(g) and U(h) is boundary-coherent,so the graph that results from pushing out this span in Graph/GT is in SGraphT (theorem 3.6.7),and so is a string graph. But this is just U(D) ,by proposition 3.3.4
Since all the morphisms are monic (and the square commutes), we can treat them as containment relations. So we will consider G and H to be subgraphs of D ,and I to be their common subgraph.
Now we note that if we have an edge eb from a !-vertex b to a vertex v in D ,and another edge e incident to v in D ,both edges must be in G or else both edges must be in H . To see this,suppose not. Then one edge (eb,say) must be in G and the other (e) in H . So v must be in I ,since it is in both G and H . But then,as g reflects ! -box containment, eb must be in I and hence in H .
We need to show that β(D) is posetal. β(D) must be simple,since if we have two edges from a ! -vertex b1 to a ! -vertex b2 in D ,they must both be in G or both in H by the above reasoning, which cannot be the case as these are !-graphs. So there are no such edges. Anti-symmetry is shown in the same way by reversing one of the edges. Reflexivity is inherited from G and H . Transitivity follows by considering that if we have the following pair of edges
they must both be in G or both in H ,and hence there must be an edge from b1 to b3 inherited from that graph. So β(D) is posetal.
Let b!(D) ,and suppose U(B(b)) is not open in U(D) . Then there is either a wire-vertex adjacent to U(B(b)) ,or a fixed-arity edge incident to it. The former case is impossible,because if we have two edges such that
where w is a wire-vertex,then ew and eb must both be in G or both be in H ,and hence there must be an edge from b to w . Similarly,if there is a fixed-arity edge e incident to v,eb and e must be both in G or both in H ,and hence there must be an edge from b to the other end of e ,and so e is not incident to U(B(b)) .
Let b,c!(D) with cB(b) ,and let vB(c) . We need to show that vB(b) . But the edge from b to c and the edge from c to v must both be in G or both be in H ,and so there must be an edge from b to v ,as required.
We now proceed to prove that all the !-box operations produce !-graphs. This theorem was stated, but not proved, in [26] (pp 7).
Theorem 4.3.4. Let G be a ! -graph and b!(G) . Then the GT! -typed graphs COPYb(G),DROPb(G) and KILLb(G) are all ! -graphs.
Proof. Corollary 4.2.4 gives us that GB(b) is a !-graph,and hence its embedding ι into G is a !-graph monomorphism. This embedding is boundary-!-coherent: since U(B(b)) is an open subgraph of U(G) ,proposition 4.1.2 gives us that U(ι) is a boundary-coherent morphism,and requirement 4 of definition 4.2.2 ensures that ι reflects ! -box containment. So we know the pushout exists in BGraphT by proposition 4.3.3,and hence COPYb(G) is a !-graph.
The DROP and KILL cases follow from lemma 4.2.3 and corollary 4.2.4 respectively.
Since one of the reaons for using string graphs is their ability to model inputs and outputs, it is useful to know how these operations affect the inputs and outputs of !-graphs. Firstly, we extend In(G) , Out(G) and Bound(G) to include !-boxes in the following way:
Definition 4.3.5. For a ! -graph G ,we define In!(G) to be the full subgraph of G containing the vertices !(G) and In(U(G)) ; Out !(G) to be the full subgraph containing !(G) and Out(U(G)) ; and Bound!(G) is the subgraph containing !(G) and Bound(U(G)) ,and any edges with a source in !(G) and a target in either !(G) or Bound(U(G)) .
These are all valid ! -graphs. Now we can show that the ! -graph operations affect the boundary in the expected manner.
Lemma 4.3.6. Let G be a ! -graph,and b!(G) ,and consider the copy operation:
Then all the maps in the pushout take inputs to inputs and outputs to outputs.
Proof. The square is symmetric, and the cases for inputs mirrors the case for outputs, so we just consider inputs for i1 and p1 .
That i1 maps inputs to inputs follows from the fact that it is boundary-!-coherent.
Suppose wIn(G) ,and consider p1(w) . If there is an edge e in COPYb(G) with t(e)=p1(w) ,
then e cannot be in the image of p1 ,since w is an input of G and p1 is injective. So e ,and hence p1(w) ,must be in the image of p2 . But then there must be a vertex w in GB(b) with i1(w)=w and p2(i2(w))=p1(w) ,since this is a pushout. w must be an input of GB(b) ,since if there were an incoming edge to w ,it would have to map to an incoming edge of w in G ,and there is no such edge. So i2(w) must also be an input of G ,since i2 maps inputs to inputs. Then i2(w) cannot have an incoming edge,and so e cannot be in the image of p2 . So there is no such edge e , and p1(w)In(COPYb(G)) .
Theorem 4.3.7. Let G be a !-graph,and b!(G) . Then
  • Bound!(COPYb(G))COPYb(Bound!(G)) ;
  • Bound!(KILLb(G))KILLb(Bound!(G)) ; and
  • Bound!(DROPb(G))DROPb(Bound!(G))
and similarly for In! and Out! .
Proof. For the COPYb case,since Bound!(G) is a ! -graph,we can construct the pushout
in BGraphT ,where D=COPYb(Bound!(G)) . This is a subgraph of COPYb(G) :
where i1G and i2G are the inclusions from the pushout that defines COPYb(G) .
Now every edge and vertex in β(COPYb(G)) is in the image of either i1G or i2G ,and its preimage is in Bound!(G) . Then it must be in the image of ι ,so D contains all ! -vertices and edges between them from COPYb(G) .
Now let w be a boundary vertex of COPYb(G) . It must have a preimage under at least one of i1G and i2G ,and lemma 3.3.9 gives us that any such preimage in G is also a boundary vertex,and hence in Bound!(G) ,and so in the image of ι . Conversely,if w is a wire-vertex in the image of ι ,it must be in the image of a boundary vertex of G under either i1G or i2G . Then lemma 4.3.6 gives us that w is a boundary-vertex of COPYb(G) .
If e is an edge from a !-vertex to a boundary vertex in COPYb(G) ,it must be in the image of either i1G or i2G ,and its preimage e under these map(s) must likewise be an edge from a !-vertex to a boundary vertex in G . So e is in Bound!(G) ,and hence in the image of ι ,and we have that ι[D]=Bound!(COPYb(G)).
For the remaining cases,we note that β(Bound!(G))=β(G) . It then follows that
β(Bound!(KILLb(G)))=β(KILLb(Bound!(G)))
and similarly for DROPb . Then the result for KILLb follows from the fact that U(B(b)) is an open subgraph of U(G) ,and DROP from the fact that it does not affect U(G) .
The arguments for In! and Out! are almost identical.

4.4 Matching String Graphs With !-Graphs

A ! -graph can be considered to be a pattern for string graphs,similar in spirit to a regular expression, although less powerful. Implicit in the term "pattern", though, is that there should be a notion of matching. We already have a notion of what it means for a string graph to match another string graph: the first string graph must be a subgraph of the second (with some additional constraints). So what does it mean for a !-graph to match a string graph?
If G is a !-graph,an obvious candidate for a string graph that should be matched by G is U(G) , the concrete part of the graph. Recalling the discussion at the start of the chapter, our aim is to match the concrete part of ! -graphs with "any number of copies" of each ! -box in G .
This is where the !-box operations come in. COPYb and KILLb provide a way of getting "any number of copies" (including zero) of the !-box B(b) . DROP b then provides a way of producing a concrete graph (which we have already noted is essentially the same as a string graph). These provide the a notion of instantiation, by which we can produce a string graph from a !-graph.
Note that this definition is slightly different to the one in [26] (pp 7). The notions of instance and instantiation in that paper correspond to concrete instance and concrete instantiation here.
Definition 4.4.1 (Instantiation). For ! -graphs G,H ,we let GH ,and say H is an instance of G ,if and only if H can be obtained from G (up to isomorphism) by applying the operations from definition 4.3.1 zero or more times. This sequence of operations is called an instantiation of H from G . If H is a concrete graph,it is called a concrete instance of G ,and any instantiation of it is also called concrete.
Remark 4.4.2. Given an instantiation S of H from G ,we will sometimes use the notation S(G) to refer to H . Note that S is not really a function: because the first operation of S refers to a 1-vertex of G,S cannot be applied to anything other than G (although we can sometimes relax this constraint in the presence of certain morphisms, as we will see in later chapters).
We can then say that a !-graph G matches a string graph H if and only if there is a concrete instance of G that matches H :
Definition 4.4.3 (Matching; [26],pp 8). Let P be a !-graph,and H a string graph. If there is a concrete instance G of P ,with instantiation S ,and a monic local isomorphism m:U(G)H,P is said to match H at m under S ,and m is said to be a matching of P onto H under S .
Note that all the !-box operations yield a pattern that is at least as specific; if we apply a !-box operation to a !-graph G to get another !-graph H ,any string graph matched by H will also be matched by G . can therefore be viewed as a refinement (pre-)ordering on !-graphs.
Given a !-graph P that satisfies a couple of constraints on !-boxes that ensure there are only ever a finite number of matchings onto any given graph (for example, there can be no empty !-boxes), it is possible to decide for any string graph G whether there is a matching of P onto G . An algorithm for this (that also produces the required instantiation) is given in chapter 7
Example 4.4.4. Suppose we wish to use a rewrite rule implementing the Z spider law to rewrite
We start by normalising the target graph:
The highlighted wire-vertices are the ones that need to be matched by vertices that are in !-boxes in the LHS of the rule. So we create four copies of b1 and two each of b3 and b4
then kill b2 and drop all the remaining !-boxes
This corresponds to the instantiation
COPYb1;COPYb10;COPYb11;COPYb3;COPYb4;KILLb2;DROPb100;
DROPb101;DROPb110;DROPb111;DROPb30;DROPb31;DROPb40;DROPb41
where,as a notational convenience,we refer to the copies of b in COPYb(G) as b0 and b1 (in abitrary order). The resulting rule matches most of the graph:
and rewriting (and removing extraneous wire-vertices) results in

4.4.1 Nested and Overlapping !-boxes

The effect of edges between ! -vertices on the ! -box operations deserves special attention. These edges can be thought of as indicating a parent-child relation, with the edge going from the parent !-box to the child !-box (although this view does not entirely hold up when we consider the self-loop that exists on each !-vertex).
The edges from a !-vertex determine which other vertices should be copied or killed when the !-vertex has COPY or KILL,respectively,applied to it. So an edge from a !-vertex b to another !-vertex c means that COPYb will also copy c (and its associated !-box).
An example that demonstrates the difference that an edge between !-vertices makes is the following:
This will match any tree of white nodes of depth at most two. However, if we remove the edge between the !-vertices, we get only the balanced trees.
The reason for this is that when we copy the outer !-box in the case where there is an edge, we also copy the inner !-box.
This produces a separate ! -box round each second-level node,allowing different numbers of nodes on different branches (eg: one could copy b20 and kill b21 ). In the case without an edge,however, copying b1 will simply extend b2 ,and every copy of b2 will have exactly one second-level node in each first-level branch of the tree.
In this case,copying or killing b2 would have the same effect on every branch of the tree,ensuring that it remains balanced.
Example 4.4.5. Recall the generalised bialgebra graph equation from the start of the chapter: Ignoring, for the moment, the details of the structure used to represent this equation (which we detail in section 5.2) we can (informally) show that the spiderised bialgebra law is an instance of this. First,we apply COPYb1 :
Next we apply COPYb2 . At this point,our shorthand !-box notation causes more confusion than it alleviates, so we use a hybrid notation where we show some of the !-box containment edges explicitly.
Finally, we DROP all the top-level !-vertices, giving us the spiderised bialgebra law.
If the !-boxes had not been nested, we would have ended up with the weaker statement

4.5 Related Work

Boneva et al describe 4 a system of graph shapes to generalise over classes of graphs in the context of model checking. Their approach is similar to the typegraph constructions we introduced for string graphs; a shape is a graph with some multiplicity constraints on edges and vertices,and a graph G is a concretisation of a shape S if there is a morphism from G to S satisfying those constraints (for example,a node of S could require that exactly 3 nodes of G map to it,or an edge could require more than 5 edges to match it). There is a shape-wide degree of approximation in these multiplicities.
The aim of graph shapes is different from that of !-graphs, even though both attempt to capture families of graphs in a single graph, and this leads to some substantial differences between them. For example, graph shapes are mostly local (although there is some weak grouping of nodes); multiplicities, in particular, are specified on a per-edge or per-node basis. !-graphs, by contrast, operate on arbitrarily-large subgraphs.
Taentzer introduced the idea of amalgamated graph transformations in [39]. These provide a framework for applying multiple, potentially overlapping, rewrite rules in parallel by identifying common sub-rules. For example, one could amalgamate two copies of the string graph rewrite rule
using the common sub-rule
to produce the familier rule
Doing this an arbitrary number of times would allow the construction of any one of the rules we intend
to represent. However, we cannot allow arbitrary amalgamations of this sort. While
are both valid rules,
certainly is not.
Rensink's nested graph transformation rules [34, 35] extend this amalgamation idea using trees of rewrite rules, each rule being a subrule of its children. A predicate language over the left-hand side of these rules allows finer control of the matching process (and, by using a tree of graphs rather than of rewrite rules, the expression of complex graph predicates).
While the predicate language is unnecessary to codify spider-like equations, the idea of rule trees could be used as a way of encoding the !-graphs we described above, even including the nesting of !-boxes. For example, using Rensink's notation, we could describe the spidered version of X copies Z using the nested graph transformation rule
The fact that an instance of this tree can have any number of copies of any given branch (including none) gives us the family of rewrite rules we desire. However, this technique could not be used to encode the generalised bialgebra law, as the tree structure does not allow for overlapping !-boxes, and hence cannot express arbitrary bipartite graphs. The approach we take (encoding !-boxes in the graph itself) also allows us to use graph rewriting to reason directly about !-graphs, as we will see in later chapters.
Stallmann produced an extension to the UML-based Story Patterns employed by FuJaBa 30 in [38]. These enhanced Story Patterns resemble Rensink's nested graph transformation rules in character, and resemble !-graphs in presentation. They allow parts of a Story Pattern to be marked with modifiers familiar from predicate logic,such as ¬ , or . For example,the following enhanced Story Pattern captures the requirement that every instance of class B is contained in an instance of class A:

Chapter 5

!-Graph Rewriting

!-graphs provide the foundation for representing infinite families of string graph equations and rewrite rules. In this chapter, we will demonstrate the construction of equations and rewrite rules composed of !-graphs and show how they can be used to rewrite string graphs, producing new string graph equations, and even !-graphs, producing new !-graph equations. Importantly, the latter is sound with respect to the interpretation of !-graph equations as families of string graph equations.
The first two sections of this chapter are again based on [26] (pp 9-11). The other two sections have not previously been published.

5.1 !-Graph Equations

We can combine ! -graphs to form ! -graph equations in much the same way we did string graph equations. We will extend the !-box operations (and hence the idea of instantiation) to these equations, and this will determine the string graph equations represented by a given ! -graph equation.
We can view a string graph equation as a pair of string graphs with correlated inputs and outputs. In the same way,we want a ! -graph equation to encode a pair of ! -graphs and a correlation of inputs, outputs and ! -vertices. For example,the spider law given in (4.1) could be represented as(5.1)
If we COPYb2,DROPb3 and KILLb4 ,we get the following equation.
The rest of this section will be devoted to formalising these constructions and showing that we can apply the !-box operations to them.
We will use a span of monomorphisms LIR ,where I equates Bound !(L) with Bound!(R) . Before we get to the technical definition, we need a short lemma.
Lemma 5.1.1. If G is a !-graph such that U(G) has no isolated wire-vertices,then we have the following pushout:
Proof. If U(G) has no isolated wire-vertices, In(U(G)) and Out(U(G)) are disjoint. The result then follows from the definitions and the fact that pushouts are unions in Graph/GT! .
The definition of a !-graph equation we give here looks quite different from the definition of a rewrite pattern given in [26] (pp 9). We are using this formulation to better demonstrate the similarities with string graph equations (definition 3.5.1), and because it is easier to use when constructing proofs.
Definition 5.1.2 (!-graph equation). A !-graph equation Li1,i2R is a span Li1Ii2R in BGraphT where
  1. U(L) and U(R) contain no isolated wire-vertices;
  1. In!(L)In!(R) and Out!(L)Out!(R) ;
  1. Bound!(L)IBound!(R) ; and
  1. the following diagram commutes,where j1,j2,k1 and k2 are the inclusions from lemma 5.1.1 composed with the above isomorphisms:(5.2)
A !-graph rewrite rule is a directed !-graph equation.
It can be seen by comparing the definitions that applying U to a 1-graph equation will yield a string graph equation, and similarly for rewrite rules.
Note that the isomorphisms in the above definition are forced to agree with i1 and i2 . In particular, lemma 5.1.1 can be used to show that the following diagram commutes(5.3)
and if we expand the definitions of j1,j2,k1 and k2 in (5.2),we get(5.4)
We will now extend the ! -box operations to ! -graph equations. The intuitive rule is that the same operation must be performed on all three graphs in the span, with the correspondence between !-boxes determined by the morphisms of the span. Of course, to get an equation, we need some way of updating the morphisms of the span in addition to the graphs.
It turns out we can do this with any monomorphism of ! -graphs that reflects ! -box containment:
Lemma 5.1.3. Let f:GH be a !-graph monomorphism that reflects !-box containment,and let b be a !-vertex in G . Then there are !-graph monomorphisms
DROPf(b)(f):DROPb(G)DROPf(b)(H)
KILLf(b)(f):KILLb(G)KILLf(b)(H)
COPYf(b)(f):COPYb(G)COPYf(b)(H)
that reflect ! -box containment and that commute with f in the following ways:(5.5) (5.6) (5.7)where i{1,2} and p1G and p2G are the maps from the pushout defining COPYb(G) :
and p1H and p2H are defined similarly.
These maps are all the unique ones satisfying these diagrams, up to unique isomorphism.
Proof. Let G=DROPb(G) and H=DROPf(b)(H) . Note that the image of G under f is contained in H ,since f is injective (so no vertex of G other than b maps to f(b) ). So there is a unique monomorphism f=DROPf(b)(f) satisfying (5.5). f reflects !-box containment,since if f(v)BH(c),f(v)BH(c) ,and cb .
Now we deal with KILLf(b)(f) . Let G=KILLb(G) and H=KILLf(b)(H) . We start by showing that the image of G under f is contained in H . These are full subgraphs of G and H , respectively,so we only need to consider vertices. Let v be a vertex in G . So v is not in B(b) . Then, since f reflects ! -box containment, f(v) is not in B(f(b)) ,and so is in H . So we can construct the monomorphism f=KILLf(b)(f) by simply restricting the domain and codomain of f . Since the inclusion of KILLf(b)(H) into H is monic,this morphism must be the unique one satisfying (5.6).
Now we show that f reflects ! -box containment. Let v be a vertex of G and c!(H) ,with f(v)BH(c) . Then f(v)BH(c) ,and so c and the edge from c to f(v) are both in the image of f . Further, c cannot be in BH(f(b)) ,since it is in H . So the preimage of c cannot be in BG(b) , and hence must be in G ,along with the joining edge,and so c and the edge from c to v are in the image of f .
Finally,we consider COPYf(b)(f) . Let G=COPYb(G) and H=COPYf(b)(H) . We demonstrate the existance of COPYf(b)(f) by pushout. If we let ιG:GB(b)G and ιH:HB(f(b))H be the natural inclusion maps, (5.6) gives us that
p1HfιG=p1HιHKILLf(b)(f)=p2HιHKILLf(b)(f)=p1HfιG
and there is then a unique f making the following diagram commute: Since all the other arrows in the diagram are monic, f must be as well. For a given choice of p1H and p2H (relative to p1G and p2G ),it is the unique morphism satisfying (5.7). If we do swap p1H and p2H , we can note that the pushout is symmetric, and pushouts are unique up to a unique isomorphism, so f is unique up to a unique isomorphism.
We must show that f reflects ! -box containment. Suppose v is a vertex in G and f(v)B(c) , where c is a !-vertex in H ,with e the edge from c to f(v) . e is in the image of one of the piH ; we call the preimage of e under it e ,and its source (which maps to c ) c.f(v) must also be in the image of iH ,and its preimage must be in the image of f . What is more,the preimage of this under f must map to v by piG ,due to (5.7).
We know that,since f reflects 1 -box containment, e must be in the image of f . But this means that e must be in the image of f ,and hence f also reflects !-box containment. So then we just let COPYf(b)(f)=f.
Given a !-graph equation Li1,i2R ,we know that i1 and i2 are isomorphisms when their codomains are restricted to Bound!(L) and Bound!(R) ,respectively. This means that they must reflect ! -box containment,so we can now make the following definitions.
Definition 5.1.4 ([26],pp 10). Let LR be a !-graph equation defined by the span Li1Ii2R , and let b!(I) ,with b1=i1(b) and b2=i2(b) . Then the !-box operations on !-graphs have the following equivalents on !-graph equations:
  • COPYb(LR) is defined to be
COPYb1(L)COPYb1(i1)COPYb(I)COPYb2(i2)COPYb2(R)
  • DROPb(LR) is the span
DROPb1(L)DROPb1(i1)DROPb(I)DROPb2(i2)DROPb2(R)
  • KILLb(LR) is the span
KILLb1(L)KILLb1(i1)KILLb(I)KILLb2(i2)KILLb2(R)
In the case of ! -graph rewrite rules,the direction is preserved in the obvious way.
Note that the equivalent definitions in [26] are the same; the definition here appears simpler because we have made use of lemma 5.1.3.
We must, of course, ensure that these operations produce !-graph equations. We start with some useful results about the operations of lemma 5.1.3.
Lemma 5.1.5. All the operations from lemma 5.1.3 respect composition, at least up to unique isomorphism. For example,
DROPg(f(b))(gf)=DROPg(f(b))(g)DROPf(b)(f)
Proof. Consider the case of DROP. Suppose we have !-box-reflecting monomorphisms
f:G1G2
g:G2G3
and suppose bG1 . Let f=DROPf(b)(f),G1=DROPb(G1) and so on. Then we just consider the diagram
But DROPg(f(b))(gf) is the unique map from G1 to G3 that makes the outside edges of that diagram commute,and so must be the same as gf . The same argument holds for KILLg(f(b))(gf) .
A similar argument can be used for COPY, but care must be taken, as the result of applying COPY to a map is only unique up to isomorphism. It is possible, however, to make the relevant choices such that COPYg(f(b))(gf)=COPYg(f(b))(g)COPYf(b)(f) ,which is sufficient to get the result we want.
Lemma 5.1.6. All the operations from lemma 5.1.3 preserve isomorphisms.
Proof. This follows from lemma 5.1.5 and the fact that DROPb(1G) and KILLb(1G) are the identity, and COPYb(1G) is an isomorphism of COPYb(G) .
Lemma 5.1.7. Let G be a graph with no isolated vertices. Then COPYb(G),KILLb(G) and DROPb(G) do not have any isolated vertices.
Proof. If w were an isolated wire-vertex in U(COPYb(G)) ,it must be the image of a map from U(G) ,but U(G) does not contain any isolated wire-vertices,and so the map must carry an incident edge with it.
U(KILLb(G)) is a full subgraph of U(G) and U(B(b)) is not adjacent to any wire-vertices,so any wire-vertex in U(G) must have the same incident edges as the corresponding wire-vertex in U(G) .
U(DROPb(G)) is isomorphic to U(G) ,and so has no isolated wire-vertices.
Theorem 5.1.8. Let LR be a ! -graph equation. Then applying any of the ! -box operations of definition 5.1.4 yields another !-graph equation.
Proof. Let Li1Ii2R be a !-graph equation,and Li1Ii2R be the result of applying one of the !-box operations to it. We will demonstrate the proof for COPYb ,but all of the arguments apply to KILLb and DROPb as well.
It is clear from lemma 5.1.3 that this is a span of !-graphs.
U(L) and U(R) do not contain any isolated wire-vertices,by lemma 5.1.7
Since Li1Ii2R is a !-graph equation,we have isomorphisms
ϕI:In!(L)In!(R)
ϕO:Out!(L)Out!(R)
ϕL:Bound!(L)I
ϕR:Bound!(R)I
These all preserve !-box containment, and hence we have isomorphisms (by lemma 5.1.6 and theorem 4.3.7)
ϕI:In!(L)In!(R)
ϕO:Out!(L)Out!(R)
ϕL:Bound!(L)I
ϕR:Bound!(R)I
Finally, we need to show that the following diagram commutes:(5.8)
where j1 is ϕL composed with the inclusion of In!(L) into Bound (R) ,and similarly for j2,k1 and k2 .
The proofs for the four triangles on the left and right are all similar, so we will demonstrate the top left triangle. Consider the following diagram:
(5.9)
where ιL:In!(L)L is the normal inclusion map. The bottom triangle commutes by lemma 5.1.5, since ιL=i1j1 by our assumption that Li1Ii2R is a 1-graph equation. That the upper right triangle commutes can be seen from the proof of theorem 4.3.7. For the upper left triangle, consider the following:
where we have abused ιL to refer to the inclusion of In!(L) into Bound!(L) . Now we can again use the proof of theorem 4.3.7 to see that the square on the left commutes, the triangle on the right commutes by lemma 5.1.5 and the definition of j1 ,and the bottom triangle is simply the definition of ϕL . But now j1 is ϕL composed with the inclusion on the left of the diagram,by definition,and so we have that the top left triangle of (5.9) commutes, and hence the upper left triangle of (5.8) commutes.
We now look at the upper middle triangle of (5.8); the lower middle triangle follows similarly. Consider the following diagram:
We have already demonstrated that the triangle on the left commutes, and the triangle on the right follows in a similar manner. The top square is just the definition of ϕI ,and the outside edges of the diagram commute by lemma 5.1.5 and the assumption that Li1Ii2R is a !-graph equation. It follows that the triangle at the bottom commutes, and this is the top middle triangle of (5.8).
Hence we have shown that Li1Ii2R is,indeed,a !-graph equation.
Corollary 5.1.9 ([26],pp 11). Let LR be a !-graph rewrite rule. Then applying any of the !-box operations of definition 5.1.4 yields another !-graph rewrite rule.
The concept of instantiation from definition 4.4.1 then extends to !-graph equations and rewrite rules in the obvious way. We will consider a !-graph equation to hold if and only if all its concrete instantiations hold.

5.2 Rewriting String Graphs with !-Graph Equations

For a !-graph equation LR and a string graph G ,we want to use the directed form of the equation,
LR ,to rewrite G ,and the resulting graph should be a valid rewrite of G in the (usually infinite) string graph rewrite system comprised of the concrete instantiations of LR .
Because applying a !-box operation to a !-graph rewrite rule also applies it to the components of that rule, and the LHS in particular, we can use the notion of matching from section 4.4 to find a concrete instance of the rewrite rule that can be applied to a given string graph G .
Suppose we have a !-graph rewrite rule LR and a string graph G . If m is a matching of L onto G under S ,we can apply S to LR to get a string graph rewrite rule LR . By considering definition 5.1.4,we can see that L is the string graph obtained by instantiating L with S . So we have a matching from L to G ,and can therefore rewrite G with LR .
Providing finding the instantiation and matching is decidable (which we demonstrate in chapter [7],rewriting G with LR is decidable,and our requirement that this is a valid rewrite under the rewrite system of instantiations of LR is satisfied.
So we have acheived our aim of expressing certain infinite families of string graph rewrite rules in a finite (and useful) way. In the next section, we will consider how !-graph rewrite rules can actually be used to rewrite !-graphs, and thereby derive new !-graph rewrite rules.

5.3 Rewriting ! -Graphs With ! -Graph Equations

Let LmG be a !-graph monomorphism. Then we have the following pushout complement(5.10)
in Graph/GT! if and only if m satisfies the no-dangling-edges condition. This condition is that for every vertex v in LBound!(L) ,and every edge e in G incident to m(v),e is in the image of m . This is stronger than U(m) being a local isomorphism,as it also requires that if a !-vertex b and a vertex v in LBound!(L) are both in the image of m ,any edge between them must also be in the image of m .
Proposition 5.3.1. If the pushout complement (5.10) exists, D is a !-graph.
Proof. As all the morphisms in the diagram are monic,we consider D and L to be subgraphs of G , and Bound!(L) their common subgraph.
Consider applying U to the pushout square. This is a pushout in Graph/GT ,by proposition 3.3.4 But pushout complements are unique up to isomorphism in Graph/GT ,and we know that the pushout complement of
Bound(U(L))U(L)U(m)U(G)
is a string graph (since U(m) is a local isomorphism,by the no-dangling-edges condition),so U(D) must be a string graph.
We apply β to the pushout square,giving us another pushout (again,by proposition 3.3.4). Then,
since β(Bound!(L))=β(L) ,we must have that β(D)β(G) ,and hence β(D) must be posetal.
Let b!(D) . Then b!(G) . We know that U(BG(b)) is open in U(G) ,and BD(b)=BG(b)D , so U(BD(b))=U(BG(b))U(D) . But this is open in U(D) by proposition 4.1.3
Let b,c!(D) ,with cBD(b) ,and let vBD(c) . Then b,c!(G) and vBG(c) ,and so vBG(b) . The edge linking b to v must either be in D or L . suppose it is in L . Then so must b and v be,and so b and v must be in Bound!(L) . But then the edge linking them must also be in Bound!(L) (by definition of Bound!) and hence in D . So vBD(b) .
So D is a !-graph.
Note that, while the no-dangling-edges condition will always produce a pushout complement, it will not always lead to a valid rewrite. For example, in the following commutative diagram in Graph /GT! ,the map on the left satisfies the no-dangling-edges condition,but the resulting (bottom right) graph is not a valid !-graph,as B(b) is not an open subgraph.(5.11)
Definition 5.3.2 (!-graph matching). A monomorphism LmG between two !-graphs is a !-graph matching when U(m) is a local isomorphism and m reflects !-box containment. If L0L ,with instantiation S,m is said to be a !-graph matching of L0 onto G under S .
Of course,if m is a ! -graph matching,then m and the inclusion of Bound!(L) in L have a pushout complement. But, unlike in (5.11), a !-graph matching always produces a rewrite.
Theorem 5.3.3. Let LR be a !-graph rewrite rule and m:LG be a !-graph matching for it. Then LR has a rewrite at m .
Proof. Let Li1Ii2R be the !-graph rewrite rule,and let
be the pushout complement of i1 and m . Then it is sufficient (by proposition 4.3.3) to show that the span formed from d and i2 is boundary-!-coherent.
Theorem 3.6.7 gives us that U(i1) and U(d) are boundary-coherent,and then lemma 3.6.8 gives us that U(d) and U(i2) must also be boundary-coherent.
i2 reflects ! -box containment by the definition of a ! -graph rewrite rule. Let e be an edge in D from a !-vertex b to a vertex v ,where v is in the image of d . Then g(v) must be in the image of m , and so g(e) must be in the image of m ,since m reflects !-box containment. But then,since this is a pushout square, e must be in the image of d as required,and so d also reflects ! -box containment. Thus d and i2 are boundary-!-coherent,as required.
Example 5.3.4. Recall the following proof from section 2.2
Consider the left equality. We can perform the equivalent rewrite by using instances of the X and Z spider laws
We can use the first of these to construct the following rewrite (ignoring issues of wire homeomorphism):
U(m) is a local isomorphism,and m can be seen to reflect !-box containment (for b1 ,in this case). As expected,we get a valid ! -graph at the end. One more application of the X spider law and two of the Z spider law will produce the chain of rewrites we want.
Suppose we have the following rewrite (where m is not necessarily a !-graph matching):(5.12)
The bottom span will almost certainly not be a !-graph rewrite rule (as U(D) will not,in general, have only isolated points), but it is trivial to produce such a rewrite rule by discarding unwanted vertices and edges from D .
Theorem 5.3.5. In (5.12),if U(G) has no isolated points then there is a subgraph J of D such that
GgJJhJH
is a !-graph rewrite rule.
Proof. We start by showing that Bound!(G) is in the image of g .
β(i1) and β(i2) are isomorphisms since i1 and i2 form a !-graph rewrite rule. It then follows from the pushout squares that β(g) and β(h) are also isomorphisms. So we must have that β(G) is in the image of g .
If w is in the boundary of U(G) ,it is either not in the image of m ,in which case it must be in the image of g ,or its preimage under m is in the boundary of U(L) (since string graph monomorphisms reflect boundaries),in which case this preimage is in the image of i1 and hence w is in the image of g . Now if b!(G) and there is an edge e from b to w in G ,we also know that if e is not in the image of m ,it must be in the image of g . So suppose e is in the image of m . Then its preimage must be in the image of i1 by the same reasoning as above,and hence e is in the image of g . So Bound !(G) is in the image of g .
We can use the same argument to show that Bound!(H) is in the image of h .
Let J be the preimage of Bound!(G) under g ,and ι:JD the inclusion of J in D.gι is monic,and hence injective,so we have JBound!(G) .
We already know that the image of β(J) under hι is β(H) ,since β(ι) and β(h) are both isomorphisms. We now show that,for all vertices w in J,h(ι(w)) is an input (resp. output) if and only if g(ι(w)) is an input (resp. output). This will then give us that the image of hι is exactly Bound!(H) (since we already know that Bound!(H) is in that image).
So let w be a wire-vertex in J . We know that g(ι(w)) is either an input or an output. Suppose it is an input (the output case is symmetric). Then ι(w) must also be an input,and if g(ι(w)) is in the image of m ,its preimage must be an input. Let w be the preimage of g(ι(w)) under mi1 . Then we know that d(w)=ι(w) and hence r(i2(w))=h(ι(w)) ,and i2(w) is an input (since i1(w) is). So the preimages of h(ι(w)) under both h and r are inputs,and hence h(ι(w)) must also be an input. If g(ι(w)) is not in the image of m ,then ι(w) is not in the image of d ,and hence h(ι(w)) is not in the image of r . Thus r cannot introduce an incoming edge for h(ι(w)) ,which must therefore be an input.
Injectivity of hι gives us the isomorphism JBound!(H) . This restricts to In!(G)In!(H) and Out!(G)Out!(H) ,as we just proved that h(ι(w)) is an input if and only if g(ι(w)) is an input. The diagram from definition 5.1.2 commutes by construction, and hence
GgιJhιH
is a !-graph rewrite rule.
Example 5.3.6. Continuing example 5.3.4 we get the following commutative diagram:
Thus we have the !-graph rewrite rule

5.4 Soundness of !-Graph Rewriting

We have shown how we can rewrite !-graphs using !-graph rewrite rules, and in doing so produce further !-graph rewrite rules. However, we also want to ensure that the resulting rewrite rule is sound with respect to its interpretation as a family of string graph rewrite rules.
Note that this differs from soundness of string graph equations or rewrite rules, as discussed in chapter 3 where soundness was with respect to a particular valuation. Instead, we are interested in soundness with respect to a particular rewrite sytem of string graphs.
Specifically,if we have a !-graph rewrite rule LR which has been used to rewrite a !-graph L to another ! -graph R ,and there is an instance of the resulting ! -graph rewrite rule LR that can rewrite the string graph G to H ,we require there to be an instance of LR that also rewrites G to H .
Luckily, not only does our definition of !-graph matching guarantee that we get a rewrite, it also ensures that we can preserve the rewrite under !-box operations. We know that the top span (L,I and R ) share ! -vertices (in that we get isomorphisms if we apply β to the maps),and the same is true of the bottom span (G,DandH; see the proof of theorem 5.3.5) . For notational convenience, we will identify the !-vertices across each of these spans (eg: if b is a !-vertex in I ,we will consider b to be in L as well,by which we mean i1(b) ).
Further,because the maps m,d and r of (5.12) are monic,we can identify each !-vertex in the top span with one in the bottom span. So, given that we wish to perform a !-box operation (which we will denote OPb ) on G and propagate it to the entire rewrite,we have two possible cases: either the !-vertex being operated on is in the image of m ,in which case we consider it as existing across the whole rewrite, or it is not, in which case it is only in the bottom span.
If b is in the image of m ,lemma 5.1.3 provides us with a way of updating all the maps of the rewrite:
OPb(L)OPb(i1)OPb(I)OPb(i2)OPb(R)
OPb(m)
(5.13)
OPb(G)OPb(g)OPb(D)OPb(h)OPb(H)
We will, of course, need to check that this is still a rewrite.
If b is not in the image of m ,lemma 5.1.3 is insufficient. However,the following lemma will allow us to extend ! -box operations on maps to ! -vertices that are not in the image of the map.
Lemma 5.4.1. Let f:GH be a !-graph monomorphism that reflects !-box containment,and let b be a ! -vertex in H but not in the image of f . Then there are ! -graph monomorphisms
DROPb(f):GDROPb(H)
KILLb(f):GKILLb(H)
COPYb(f):GCOPYb(H)
that reflect ! -box containment and that commute with f in the following ways:(5.14) (5.15) (5.16)
where i{1,2} and p1H and p2H are the maps from the pushout that defines COPYb(H) .
Proof. Since b is not in the image of f (and so neither are any of its edges),we let DROPb(f) be f ,but with codomain DROPb(H) . Simply restricting the codomain cannot break the property of reflecting ! -box containment,so this is inherited from f .
KILLb(f) follows in the same way once we note that,since f reflects ! -box containment,the image of f cannot intersect B(b) .
Recall the definition of COPYb(H) :
Let ι be the induced inclusion of HB(b) into COPYb(H) (equal to both composed maps in the diagram). Now we define
COPYb(f):=ιKILLb(f)
and so we have a monomorphism that satisfies (5.16). For the remainder of this proof, we will use f to refer to COPYb(f) for convenience.
Let v be a vertex in G and e an edge from a !-vertex b to f(v) in COPYb(H) . e must be in the image of at least one of the piH . Then (one of) its preimage(s) e is an edge from a !-vertex to f(v) in H ,and so e must be in the image of f (as f reflects !-box containment). So e is in the image of f ,and hence f also reflects ! -box containment.
Armed with this result,if b is not in the image of m ,we can do the following:(5.17)
which we again need to show is a rewrite. The first step (for both (5.13) and (5.17)) is to show that the ! -box operations preserve the property of being a ! -graph matching.
Lemma 5.4.2. Let f:GH be a ! -graph matching and let b be a ! -vertex in H . Then DROPb(f) , KILLb(f) and COPYb(f) are all ! -graph matchings.
Proof. Lemmas 5.4.1 and 5.1.3 give us that they are monomorphisms that reflect !-box containment.
So we just need to show that they are local isomorphisms.
U(DROPb(f))=U(f) ,which we already know to be a local isomorphism.
If b is not in the image of f ,we note that since f reflects ! -box containment,the image of f cannot intersect B(b) . Then,since simply restricting the codomain cannot break the property of being a local isomorphism, U(KILLb(f)) must be a local isomorphism,since U(f) is.
Otherwise,suppose b is in the image of f ,and U(KILLb(f)) is not a local isomorphism. Let n be a node-vertex in the image of KILLb(f) with an incident edge e not in its image. We know that e is in the image of f ; let its preimage be e . Then the end of e that does not map to n must be in B(b) ; call this vertex v . But,since f(b)=b ,we must have that f(v)B(b) ,and so e cannot be in KILLb(H) and hence there can be no such n . So U(KILLb(f)) is a local isomorphism when U(f) is.
Now we just have to deal with COPYb(f) . For convenience,we will call this f for the remainder of the proof.
Suppose b is not in the image of f ,and U(f) is not a local isomorphism. So there is a node-vertex n in U(G) such that U(f)(n) is incident to an edge e not in the image of U(f) . e must be in the image of at least one of the piH . Call (one of) its preimage(s) e . Then e must not be in the image of U(f) (since otherwise e would be in the image of U(f) ). But e is incident to U(f)(n) ,and so U(f) is not a local isomorphism. Contrapositively,if U(f) is is a local isomorphism,then so is U(f) .
Now suppose b is in the image of f . Let n be a vertex in COPYb(G) with an edge e incident to f(n) in U(COPYb(H)).e is in the image of one of the piH ; call the preimage of e under it e.f(n) must also be in the image of piH ,and its preimage must be in the image of f . What is more,the preimage of this under f ,which we will call n ,must map to n by piG .
We know that,since U(f) is a local isomorphism,all the incident edges of U(f)(n) must be in the image of U(f) ,including e . So e is in the image of piHf ,and hence in the image of fpiG . So e is in the image of f ,and hence U(f) is a local isomorphism.
We know that the two squares of (5.13) commute (up to an isomorphism) by lemma 5.1.5 For (5.17), we need the following lemma:
Lemma 5.4.3. If f:G1G2,g:G2G3 and h:G3G4 are !-graph monophisms that reflect
!-box containment,and b is a !-vertex of G3 not in the image of g then
DROPb(gf)=DROPb(g)f
and
DROPh(b)(hg)=DROPh(b)(h)DROPb(g)
and similarly for KILL and COPY.
Proof. We can deduce the first DROP case from the following diagram, where the right and outer triangles commute by definition, and hence the left triangle commutes, since the inclusion map on the right is monic.
The second drop case follows in the same way from
and the KILL cases use the same argument.
For COPY,we recall that COPYb(gf) is defined to be ι3KILLb(gf) ,where ι3:KILLb(G3) COPYb(G3) is the inclusion map induced by the pushout square that defined COPYb(G3) . We know that this is then ι3KILLb(g)f ,which is COPYb(g)f as required.
From the proof of 5.1.3 we note that
COPYh(b)(h)ι3=ι4KILLh(b)(h)
where ι4:KILLb(G4)COPYb(G4) is defined similarly to ι3 . Then we have
COPYh(b)(hg)=ι4KILLh(b)(hg)
=ι4KILLh(b)(h)KILLb(g)
=COPYh(b)(h)ι3KILLb(g)
=COPYh(b)(h)COPYb(g)
From this, we can deduce that the two squares of (5.17) commute. All we need now is that both squares in each diagram are pushouts. For this, we recall that pushouts of graphs are just unions of graphs. So a commuting square of monomorphisms
is a pushout if and only if h and i cover D and the image of hf=ig is exactly the intersection of the images of h and i . To get that this is the case for (5.17),we use the following lemma.
Lemma 5.4.4. Let f:GH be a !-graph monomorphism that reflects !-box containment,and let b!(H) . If ιD:DROPb(H)H is the normal inclusion,then for any vertex or edge x of DROPb(H),ιD(x) is in the image of f if and only x is in the image of DROPb(f) ,and similarly for KILLb ,and if piH:HCOPYb(H) is one of the pushout maps from the definition of COPYb(H) , for any vertex or edge x of H,piH(x) is in the image of COPYb(H) if and only if x is in the image of f .
Proof. If b is not in the image of f ,the arguments for all the operations are very similar; we will use DROP as the example. We know that the following diagram commutes (from lemma 5.4.1): Let x be a vertex or edge of DROPb(H) . If x is in the image of DROPb(f),ι(x) must be in the image of f by commutativity of the diagram. Conversely,if ι(x) is in the image of f ,its preimage must map to x under DROPb(H) ,since ι is monic (and hence injective) and the diagram commutes.
So suppose b is in the image of f ,and let b be its preimage. We will start with the DROP case again. We have the following diagram (from lemma 5.1.3):
If x is a vertex or edge of DROPb(H) that is in the image of DROPb(f) ,then ιH(x) is in the image of f ,by commutativity of the diagram. For the converse,we will consider vertices and edges separately.
Suppose v is a vertex of DROPb(H) with ιH(v) in the image of f . Since f is monic,there is a unique v with f(v)=ιH(v) . Now ιH(v) cannot be b ,so v cannot be b ,and hence v is in the image of ιG . But then the preimage of v under ιG must map to v by DROPb(H) ,since all the maps are monic and the diagram commutes,so v is in the image of DROPb(H) .
Now suppose e is an edge of DROPb(H) with ιH(e) in the image of f . Again,there is a unique preimage e under f ,and the same must be true of the endpoints of the edge. So,by what we have already proved,the endpoints of e must be in the image of ιG ,and hence e must be (since ιG is full in G ),and we have what we require by commutativity of the diagram.
The KILL case is almost identical,except that in the vertex case,we must note that v is not in B(b) ,as v is not in B(b) .
The COPY case is also similar. This time we have the following diagram (actually two diagrams, with i{1,2}) .
As in the DROP case,if x is a vertex or edge of H that is in the image of f ,then piH(x) is in the image of COPYb(f) .
Suppose v is a vertex of H with p1H(v) in the image of COPYb(f) ,which we will denote f (the case for p2H is similar). We then have a vertex v of COPYb(G) that maps to p1H(v) by f . Now v is in the image of at least one of p1G and p2G . If v is in the image of p2G ,consider its preimage u in G.f(p2G(u))=p2H(f(u))=p1H(v) ,and hence v and f(u) are both in the image of the inclusion ιH:HB(b)H ,by the pushout that defines COPYb(H) ,with a common preimage. But this means they must,in fact,be the same vertex,and hence v is in the image of f . The only other option is that v is in the image of p1G ; we will again call the preimage u . But then we have f(u)=v by the above diagram of monomorphisms,and so v is in the image of f .
Theorem 5.4.5. Consider the following rewrite,where m is a !-graph matching,
and let b be a !-vertex of G (we will also consider it to be a !-vertex of D and H ). Then for any !-box operation OPb on b ,if b is not in the image of m ,the following is a rewrite
and if b is in the image of m ,we consider it to be a !-vertex of L,I and R ,and the following is a rewrite:
Proof. We have already established that both of these are commuting diagrams of !-graph monomor-phisms,that the top span in each diagram is a !-graph rewrite rule and that OPb(m) is a !-graph matching. All we have left to show is that all the squares are pushouts.
We will first consider the DROPb case. Let ιG:DROPb(G)G be the inclusion map,and similarly for the other ! -graphs. Suppose we have a vertex or edge x in DROPb(G) . Then ιG(x) must be in the image of at least one of m or g ,and so x must (by lemma 5.4.4) be in the image of at least one of DROPb(m) or DROPb(g) . So these maps cover DROPb(G) . If x is in the image of both these maps, ιG(x) must be in the image of both m and g . Let x be the preimage of x under DROPb(g) . Then ιD(x) is the preimage of ιG(x) under g ,which is in the image of d ,since this is a pushout of graphs. But then applying lemma 5.4.4 again gives us that x must be in the image of DROPb(d) . Then commutativity of the diagrams and the fact that all the maps are monic gives us that the preimage of x under DROPb(m) must be in the image of i1 or DROPb(i1) (depending on whether b is in the image of m ). So DROPb(m) and DROPb(g) intersect exactly on the part of the graph mapped to from I (or DROPb(I) ),and so the left part of the diagram is a pushout. The same argument applies to the right squares,and so we have the result for DROPb . KILLb follows in the same way.
The argument for COPYb is similar; here we have to note that if we have x in COPYb(G) ,it must be in the image of at least one of the pushout maps from G that define COPYb(G) . We can call this map p1G and its preimage x . Then,as before,we use lemma 5.4.4 to get that x is the in the image of at least one of COPYb(m) or COPYb(g) ,since x is in the image of at least one of m or g . Similarly,if x is in the image of both maps,it must be the image of something in COPYb(I) or I (depending on whether b is in the image of m ) since then x is in the image of both m and g and is hence the image of something in I .
In the above theorem,let GH be the induced !-graph rewrite of the span GDH in the rewrite. It should be clear that the rewrite rule induced by the span
OPb(G)OPb(g)OPb(D)OPb(h)OPb(H)
is exactly the result of applying OPb to GH . So we have that if GH is a !-graph rewrite derived from a rewrite LR,OPb(GH) is derived from either LR or OPb(LR) ,and hence have the following corollary:
Corollary 5.4.6. Suppose LR is a !-graph rewrite rule that rewrites G to H at a !-graph matching,and GH is the associated ! -graph rewrite rule. Then for any concrete instance GH of this rule,there is a concrete instance of LR that rewrites G to H ,and the associated string graph rewrite rule GH is a concrete instance of GH .
This is the semantics of rewriting ! -graphs using ! -graph rewrite rules: that the rewrite holds for all concrete instances of the rewritten graphs. In this way, just as !-graph rewrite rules allowed us to represent inifinitely many string graph rewrite rules at once, !-graph rewriting allows us to do infinitely many string graph rewrites at once.
It is important to note that if we can apply an instantiation to a rewrite, we can apply it to a sequence of rewrites. If we consider two consecutive rewrites
GHJ
then we know that G and H contain the same ! -vertices,and the same goes for H and J . If we can instantiate GH to GH ,applying the same instantiation to HJ will produce a rewrite from H to some graph J ,so we will have a rewrite sequence
GHJ
If we perform COPYb1 and KILLb4 ,we get the following rewrite:

Chapter 6

A Logic of ! -Graphs

In this chapter, we will use the results of chapter 5 to build a logic of !-graphs that can be implemented by a computer, using graph rewriting as the core operation. This will include an equational logic much like that in section 3.5 together with some inference rules that build on that foundation.
In the term world, these rules would be based on predicates involving logical operators rather than purely on equations (although an equation is, of course, a type of predicate). For example, a -introduction rule might state that if you can provide a proof of a predicate P and a proof of a predicate Q ,you can deduce that there is a proof of the predicate PQ . This would be written
PQPQ
Another common rule is induction,where P is a predicate over the natural numbers (or some other well-founded set):
P(0)P(n)P(n+1)n.P(n)
Our graphical language does not contain logical connectives, nor does it contain the natural numbers used in the above induction rule. However, !-boxes do induce a well-founded structure amenable to a graphical analogue of induction. In this chapter, we will present this and other rules, and prove their soundness.

6.1 !-Graph Equational Logic

Let E be a set of !-graph equations. Our equational logic should look very familiar:
(Axiom)Gi,jHEEGi,jH(Reft)EGbG,bGG(Sym)EGi,jHEHj,iG
(TRANS)EGi,jHEHk,lKEGp,qK(LEIBNIZ)EGi,jHEGi,jH
(HOMEO)EGi,jHEGi,jH
where p:=i and q:=lk1j ,
is a !-graph rewrite (where, in particular, all morphisms reflect !-box containment), and
GiIjH and GiIjH
are wire-homeomorphic.
To these, we add inference rules for instantiations of !-graph equations:
(CoPY)EGi,jHECOPYb(Gi,jH)(DROP)EGi,jHEDROPb(Gi,jH)
(KILL)EGi,jHEKILLb(Gi,jH)
Since our rewriting process implements AXIOM and LEIBNIZ up to wire homeomorphism and up to instantiation of ! -graph rewrite rules,the above logic is equivalent to the relation E .
For a set of ! -graph equations E ,let E~ be the set of concrete instances of the equations of E . Then the semantics of EGH we use is that,for any concrete instance GH of GH ,
E~GH
in the equational logic of string graphs. Soundness of the above logic with respect to these semantics follows from corollary 5.4.6 and the fact that string graph rewriting implements the equational logic for string graphs.

6.2 Regular Forms of Instantiations

A lot of the proofs in this chapter rely on reasoning about instantiations. However, multiple instantiations can produce the same instance of a !-graph, making them harder than necessary to reason about. In particular, copying a !-box and then killing one of the copies results in the original graph (up to isomorphism).
In this section, we will demonstrate that it is possible to, if not completely remove these re-dunancies from the set of allowed instantiations, at least require a certain structure that is easy to reason about without affecting the set of possible instances of a !-graph.
We will concentrate on instantiations of ! -graphs,but the results extend to ! -graph equations.

6.2.1 Depth-Ordered Form

Definition 6.2.1 (Depth). Let b be a !-vertex of a !-graph,and P(b)=pred(b)b the set of parent !-vertices of b . Then the depth of b is defined by
δ(b)={0P(b)=1+max{δ(c)cP(b)} otherwise 
The depth of a !-box operation is the depth of the !-vertex it operates on.
Another way of viewing the depth of a !-vertex is that it is the longest ancestor-path to a top-level !-vertex.
We can now define a depth-ordered form for instantiations.
Definition 6.2.2 (Depth-ordered form). A instantiation is depth-ordered if no !-box operation of depth n is preceded by an operation of depth greater than n .
So a depth-ordered instantiation has some number of !-box operations of depth 0 , followed by some number of depth 1 , then of depth 2 and so on.
We will demonstrate that any instantiation has a depth-ordered form that is equivalent in the sense that the resulting graphs are isomorphic. To do this, we will present an algorithm that converts any instantiation into a depth-ordered one, where each change that the algorithm makes preserves the resulting graph.
We will need some results about what changes we can make, but first we need a way to talk coherently about those changes. For example, most of the changes we make will be commuting two operations in an instantiation.
An instantiation is a sequence of operations that progressively transforms a graph. The operations in that sequence cannot be divorced from the graphs they operate on. Consider an intermediate stage of a hypothetical instantiation; the operations up to this point have produced the graph
Suppose that the next operation in the sequence is COPYb . Then the next intermediate graph will be
The depth of b in G1 ,and hence of COPYb ,is 1 . If the next operation is DROPc ,it will have depth 0 , so the sequence cannot be depth-ordered.
What we would like to do is exchange the order of COPYb and DROPc ,while still reaching the same graph G3 :
G3=[000];OO
However, c is a vertex of G2 ,and does not actually exist in G1.c is derived from a !-vertex of G1 , though; which !-vertex is obvious from the pictures of the graphs.
More generally,we can construct a morphism from G2 to G1 that maps each vertex or edge to the one it was derived from.
Definition 6.2.3 (Origin Map). Let G1 be a !-graph, b!(G1) and G2=COPYb(G1) . Then f:G2G1 ,as defined by the following pushout:(6.1)
is called the origin map for COPYb .
The origin maps for KILLb(G1) and DROPb(G1) are the natural inclusion morphisms into G1 (which exist because these operations are graph subtractions).
Armed with the origin map f:G2G1 ,we can apply DROPf(c) to G1 ,obtaining another graph G2 :
Now we need to find the !-vertex of G2 that corresponds to b . In this case,since the origin map of a DROP operation is injective and b is in its image,it has a unique preimage b in G2
and we can apply COPYb to G2 to get a graph G3
which is clearly isomorphic to G3 ,and the origin maps for both sets of sequences are the same. COPYb and DROPc are an example of commutable operations.
Definition 6.2.4 (Commutable operations). We say a sequence of two operations OPb1;OPc2 (with origin maps f1 and f2 ,respectively) is commutable when c is the only vertex that maps to f1(c) under f1 and b has a unique preimage under f2 ,the origin map of OPf1(c)2 .
Note that whether two operations are commutable depends on the !-vertices they operate on. Of course, if we say that the operations are commutable, we expect them to have the same result in either order.
Proposition 6.2.5. Let H1 be a ! -graph, b!(H1),H2=OPb1(H1) with origin map f1,c!(H2) and H3=OPc2(H2) with origin map f2 . If OPb1 and OPc2 are commutable with commuted form OPc2;OPb1 (with origin maps f2 and f1 respectively) resulting in H3 ,then H3H3 ,and this commutes f1f2 and f2f1 .
Proof. If both operations are DROP or KILL, we just note that the net effect is to remove the union of the subgraphs,regardless of the order. For example,if OP1 is DROP and OP2 is KILL,
H3=H3=H1({b}B(f1(c)))
If OP1 is COPY,the conditions on commutable operations mean that f1(c)B(b) . Suppose OP2 is DROP. Consider the effect of DROPf1(c);COPYb on H1 :
Since (H1{f1(c)})B(b)=(H1B(b)){f1(c)},H3 must be the same as H3 ,ie: COPYb(H1){ι(f1(c))} ,where ι is the inclusion of H1B(b) into COPYb(H1) .
A similar argument works when OP2 is KILL. We have
and,because every vertex in B(ι(f1(c))) in COPYb(H1) must be in B(f1(c)) in all copies of H1 it is contained in, H3 must again be the same as COPYb(H1)B(ι(f1(c))) .
These arguments also work when OP2 is COPY and OP1 is DROP or KILL. That just leaves the case where both operations are COPY.
In their original order, we have two pushouts:
Note that the requirements for commutability of operations mean that c is in the image of both p1 and p2 ,and b is likewise in the image of both p1 and p2 . We construct the isomorphism from H3 to H3 by initially constructing a bijective map ϕv from the vertices of H3 to the vertices of H3 .
Let v3 be a vertex of H3,v2=f2(v3) and v1=f1(v2) . We then choose v2 to be p1(v1) if v3 is in the image of q1 and p2(v1) if v3 is in the image of q2 . Likewise, v3=q1(v2) if v2 is in the image of p1 and v3=q2(v2) if v2 is in the image of p2 . We then set ϕv(v3)=v3 .
First,we need to check that we have defined a coherent function. If v3 is in the image of both q1 and q2,v2 cannot be in B(c) . Then v1 is not in B(f1(c)) ,since if it were,whichever of p1 and p2 maps v1 to v2 must also map the edge from f1(c) to v1 to an edge from c to v2 . Thus p1(v1)=p2(v1) . Likewise,if v2 is in the image of both p1 and p2,v2 cannot be in B(b) and q1(v2)=q2(v2) . So ϕv is a valid function.
Note that the definition of an origin map means that f1(v3)=v2 and f2(v2)=v1 . Thus the same construction works in reverse,allowing us to construct the inverse map ϕv1 ,and so ϕv is a bijection.
Since !-graphs are simple,we just need to show that,for any two vertices v3 and w3 of H3 ,there is an edge from v3 to w3 if and only if there is one from ϕv(v3) to ϕv(w3) . We construct a w family of vertices in the same way we constructed the v family.
If there is an edge e3 from v3 to w3 ,this edge is mapped to an edge e1 from v1 to w1 by f1f2 . The existence of e3 means that v3 and w3 must both be in the image of q1 or both be in the image of q2 . Thus v2 and w2 must both be in the image of p1 or both be in the image of p2 ,and that morphism must map e1 to an edge e2 from v2 to w2 . Similarly,either q1 or q2 must map e2 to an edge from v3 to w3 .
The converse case is symmetric,and hence ϕv extends to an isomorphism ϕ:H3H3 .
We have generalised commutable operations beyond just being on entirely separate parts of the graph, like in the example above, but we still have to deal with non-commutable operations. If the operations are already depth-ordered,such as if the next operation were DROP e
we can safely ignore them.
Instead, we will look at operations where the preimage of the !-vertex the second operation acts on is a parent of the !-vertex the first acts on. For example,suppose the next operation on G2 were KILLd . Then the operations would not be depth ordered (KILLdhas depth 0,likeDROPc did, while COPYb has depth 1),but they cannot be commuted; once again, b is not in the image of the origin map of KILLf(d) .
00
In this case,we can simply discard the COPYc operation,since KILLd is clearly isomorphic to KILLf(d) . The same would be true if the first operation were DROPc or KILLc .
Lemma 6.2.6. Let H1 be a ! -graph, b!(H1),H2=OPb(H1) with origin map f,c!(H2) and H3=KILLc(H2) with origin map k ,where bB(f(c)) . Then H3 is isomorphic to KILLf(c) (with origin map k ),and this isomorphism commutes k and fk .
Proof. If OP is DROP or KILL,this has the same net effect,since bB(f(c)) and hence B(b) B(f(c)) . If it is COPY,it is sufficient to note that
H1B(f(c))H1B(b)
and hence the COPY operation has no effect on the part of the graph preserved by the KILL operation.
If the next operation is COPYd,b will have two preimages under the origin map of COPYf(d) , which we will call b0 and b1 . Then the replacement sequence will be
COPYf(d);COPYb0;COPYb1
Lemma 6.2.7. Let H1 be a ! -graph, b!(H1),H2=OPb(H1) with origin map f,c!(H2) and H3=COPYc(H2) with origin map g ,where bB(f(c)) .
Let H2=COPYf(c)(H1) ,with origin map g . Then b has two preimages under g,b0 and b1 . Let H3=OPb0 ,with origin map f0.b1 has a unique preimage under f0 ,which we call b1 . Let H4=OPb1 ,with origin map f1 . Then H4 is isomorphic to H3 ,and this isomorphism commutes fg and gf0f1 .
Proof. Intuitively,whatever we did to b before the COPY operation,we do instead to both copies of b after it.
If OP is DROP,we remove both b0 and b1 ,and this is the same as removing just b before applying the COPY. If OP is KILL,the preimage of B(b) under g is exactly the union of B(b0) and B(b1) ,and hence the net effect is likewise maintained. We note that B(b0)B(b1)= ,and then the COPY case follows from a similar proof to that of two commutable COPY operations (in proposition 6.2.5).
We have not dealt with the second operation being DROPd ,because this commutes with COPYc , and indeed DROP commutes with any preceding operation on a distinct !-vertex, including child !-vertices.
When we are dealing with rewrite sequences longer than two operations, explicitly referring to the origin maps will become extremely cumbersome. Therefore,if we have an origin map f:G2G1 and a !-vertex b of G1 with a unique preimage under f ,we will also refer to this preimage as b . If it has two preimages under f ,we will refer to one as b0 and the other as b1 .
We can now set out algorithm 1 which takes an arbitrary instantiation of a !-graph and gives a depth-ordered one that produces the same graph.

Algorithm 1 Order !-box operations by depth
while has unmarked operations do
op rightmost unmarked operation
b !-box op operates on
look at op ,immediately to right of op ,operating on b
if there is no such op then { case 1 }
mark op
else if δ(b)δ(b) then { case 2 }
mark op
else if b is not a parent of b then { case 3 }
commute op and op
else if op is KILL then { case 4 }
discard op
else if op is DROP then { case 5 }
commute op and op
else if op is COPY then { case 6 }
remove op and add two copies of op to the right of op ,acting on the two copies of b
end if
end while

The preceding discussion gives rise to the following proposition, stating that the algorithm does not alter the effect of the instantiation:
Proposition 6.2.8. Applying algorithm 1 to an instantiation that results in a graph G yields (if it terminates) an instantiation that results in a graph isomorphic to G .
The main invariants of the algorithm are that the marked operations are depth-ordered relative to each other,and that no unmarked operation of depth d is ever to the right of a marked operation of depth >d . This can be seen by noting that op is always unmarked and everything to the right of it,including op ,is marked. The first part of the invariant is preserved because the algorithm never alters the order of the marked operations, and an operation is only marked when the marked operations to its right have the same or greater depth (and the second part of the invariant requires that the marked operations to the left have the same or lesser depth). The second part of the invariant is maintained because we only ever move op to the right of op when δ(op)>δ(op) and while this can reduce the depth of op ,it can only reduce it to δ(op) .
Proof. We will place a (tight) upper bound on the number of iterations, as well as on the length of the final instantiation. Specifically, given the recurrence relations
s0=0
si+1=si+2si
c0=0
ci+1=ci+2si1
we will show that if the input instantiation is of length i ,the output instantiation is no longer than si operations and the algorithm takes no more than ti=ci+si iterations. We will do this by induction on i . The i=0 case is trivial.
The main thing to note for the step case is that if we have the instantiation S=OPb;T ,because the algorithm always deals with the rightmost unmarked operation (and the operation to its right), it will not consider OPb until it is the last remaining unmarked operation. This means that the first part of a run of the algorithm on S is the same as a run of the algorithm on T .
So suppose the length of S is i+1 . By the inductive hypothesis,after at most ti iterations, the instantiation will look like OPb;T ,where T consists of at most si marked (and no unmarked) operations,and OPb remains unmarked.
Let l be the actual length of T . We will show that after at most 2l1 iterations that hit cases 3-6, the instantiation will be depth-ordered. Since only case 6 iterations can introduce new operations,and only one at that,there can be at most 2l case 1 or 2 iterations before the entire sequence is marked. So there are at most l+2lsi+2si operations in the final sequence,and at most
ti+2l+2l1=si+2l+ci+2l1si+1+ci+1=ti+1
iterations in total.
We need to note here that any operations in the sequence, marked or unmarked, at any subsequent point that are not part of T must be OPb or a copy of OPb . If two copies of OPb are adjacent,they must have the same depth. This is because the depth of a copy of OPb can only be changed by being commuted with a DROPc . But any other copy of OPb adjacent to it must have been commuted with the same DROPc ,and its depth will have been changed in the same way. It follows that cases 3-6 can only be triggered if op is a member of T .
Suppose we are at some iteration of the algorithm (at or after the point where we have OPb;T ). Consider op ,the rightmost unmarked operation in the sequence. Call the subsequence to the left of op S1 ,and the subsequence to its right S2 ,so the whole sequence is S1;op;S2 . Let n be the number of operations of T that are in S2 .
We will show by induction on n that,in no more than 2n1 case 3-6 iterations (and some number of case 1 or 2 iterations),the instantiation will be S1 followed by marked operations.
For n=0 ,either S2 is empty,in which case we trigger case 1 and are done,or S2 consists only of operations derived from OPb ,which must therefore have the same depth as op. This means we trigger case 2, and again are done.
Suppose n=k+1 . If cases 1,2 or 4 are triggered,we are done. Cases 3 and 5 require the inductive hypothesis, but are straightforward. So suppose we hit case 6. We now get two copies of op ,each of which has k operations from T to the right of it. We apply the inductive hypothesis to the right hand one to get that in at most 2k1 case 3-6 iterations,the left hand one will be the rightmost unmarked operation. As already discussed,this will still have k operations from T to the right of it,so after no more than 2k1 further case 3-6 iterations,we will have the sequence we want ( S1 followed by only marked operations). Then we see that
1+(2k1)+(2k1)=2k+11
which is what we wanted.
Corollary 6.2.10. Any instance H of a !-graph G has a depth-ordered instantiation.
The upper bound for this algorithm may appear worryingly high, but it is not an algorithm that would ever be implemented. The fact that such an algorithm exists, however, allows us to assume that any instantiation is depth-ordered; if it is not, we can produce an equivalent one that is. In fact, in chapter 7 we will demonstrate matching techniques that directly produce depth-ordered instantiations.

6.2.2 Expansion-Normal Form

A depth-ordered concrete instantiation has only operations of depth 0 . To see this, note that any operation of depth greater than 0 must be on a !-box that has one or more parents, and at least one of those parents must be of depth 0 (by posetality of the subgraph of !-vertices). However, since the instantiation is depth-ordered,there can be no further operations on that ! -box,and so it must exist in the final graph, which cannot then be a concrete graph. So the instantiation cannot be concrete.
We will introduce EXPb as a shorthand for COPYb;DROPb1 . As a notational convenience,we will consider b0 to be the same as b ,since it is the unique preimage of b under the composition of the origin maps.
Definition 6.2.11 (Expansion-normal form). A concrete instantiation is in expansion-normal form when it is composed entirely of EXP and KILL operations, and the depth of every operation is 0 . Example 6.2.12. A sequence in expansion normal form:
Every operation is on a top-level !-box (depth 0), and the only operations are EXP and KILL.
We generally identify the "constant" parts of the graph for each operation (in a manner consistent with the origin maps), and view EXP operations as adding to the graph and KILL operations as removing part of the graph.
Theorem 6.2.13. Any concrete instance H of a 1-graph G has an instantiation in expansion-normal form.
Proof. We know from corollary 6.2.10 that there must be a depth-ordered instantiation of H from G ; we will transform this into an equivalent instantiation (ie: resulting in the same graph,up to isomorphism) that is in expansion-normal form.
In order to do this,we will need to be able to,for a given COPYb operation,move any operation on b0 or b1 to immediately after COPYb . We will demonstrate this for arbitrary depth-ordered instantiations, not just concrete ones.
Consider an operation OPb0 (recalling that b0 and b1 are arbitrary labels,and hence inter-changable). The depth of OPb0 must be the same as the depth of COPYb . The only way the depth of OPb0 could deviate from that of COPYb is if there were a DROP operation between them on a parent of b0 . But the depth of this DROP operation would have to be strictly less than the depth of COPYb ,which contradicts the depth-ordering. Indeed,there can be no operations on any parent of b0 after COPYb .
Similarly,there can be no operations on any child of b0 between COPYb and OPb0 ,since that operation would have a depth strictly greater than that of b0 ,and hence of OPb0 ,which violates depth-ordering. Therefore,proposition 6.2.5 allows OPb0 to be freely exchanged with the operation preceeding it until it reaches COPYb ,and this will maintain the depth-ordering of the sequence.
Note that this also allows us to move EXPb0 back,since we can move COPYb0 back to COPYb , and then move DROPb01 back to COPYb0 . Likewise,given EXPc ,we can move any subsequent EXPc back to join it,so we can move all occurrences of EXPb0 and EXPb1 to immediately follow COPYb .
Starting with a depth-ordered concrete instantiation, we can eliminate COPY (in favour of EXP) with the following procudure (note that we treat EXP as an opaque operation in its own right, not a composite of COPY and DROP), and so obtain a concrete instantiation in expansion-minimal form.
We eliminate COPY operations starting from the right. At each stage, we consider the rightmost COPY operation, COPYb . If the next operations on b0 and b1 are both EXP,we first move all the EXPb0 and EXPb1 operations to immediately after COPYb . We then replace all the EXPb1 operations by EXPb0 ,which is an equivalent operation in this context.
This done,we know that,after COPYb ,the first operation on b1 must be either KILLb1 or DROPb1 . In both cases,we move it back so that it immediately follows COPYb . In the case of DROPb1 ,we can just replace both operations with EXPb (and replace all later references to b0 with b ). Since COPYb was depth 0,EXPb must also be depth 0 . In the case of KILLb1 ,we can eliminate both operations (and,again,replace all later references to b0 with b ). Then we will have eliminated this occurrence of COPY, and we can proceed onto the next rightmost occurrence, until none remain.
Once we have eliminated all occurrences of COPY, we can eliminate DROP operations by replacing each DROPb with EXPb;KILLb ,which both have depth 0 since DROPb does. EXPb;KILLb is COPYb;DROPb0;KILLb1 ,and this is equivalent to COPYb;KILLb1;DROPb0 ,which is equivalent to DROPb .
So we now have a concrete instantiation containing only EXP and KILL operations, and all the operations are of depth 0 , so it is in expansion-normal form.
Once we have an instantiation in expansion-normal form,if b is a top-level ! -vertex in the starting graph G ,we can pull all the operations on b to the start of the instantiation. So the instantiation will start with some number of EXPb operations,followed by KILLb (the argument for this is identical to the one that allowed us to move operations on b0 back to COPYb ).

6.3 !-box Introduction

We will demonstrate a simple inference rule that allows us to wrap an entire !-graph equation in a !-box.
Definition 6.3.1 (BOX). Suppose G is a 1-graph. Then BOX(G) is the GT! -typed graph consisting of G together with a fresh ! -vertex b and an edge from b to every vertex in the graph (including itself).
Example 6.3.2. If we consider the graph G : then BOX(G) is
We will sometimes write BOXb(G) to specify a name for the fresh !-vertex; in contrast to the other ! -box operations, b is not in !(G) but is in !(BOXb(G)) .
BOX(G) is easily seen to be a !-graph: U(BOX(G))U(G) and hence is a string graph; extending a poset with a fresh element that is every element of the poset and to itself yields another poset; U(BBOX(G)(c))U(BG(c)) for every c!(G) and U(B(b))U(G) ,so these are all trivially open subgraphs of U(BOX(G)) ; and cB(c)B(c)B(c) follows from the fact this is true for G and B(b)=BOX(G) .
As with the other operations, we can apply BOX to monomorphisms that reflect !-box containment:
Proposition 6.3.3. Let f:GH be a monomorphism in BGraphT that reflects ! -box containment. Then f can be uniquely extended to a !-box-reflecting monomorphism BOX(f):BOX(G) BOX(H) that commutes with the inclusions of G into BOX(G) and H into BOX(H) .
Further,if g:HK is another such morphism, BOX(gf)=BOX(g)BOX(f) .
Proof. If we have BOXb(G) and BOXc(H) ,the only possible extension of f is the one that maps b to c ,and maps each edge between b and some vertex v in BOXb(G) to the edge from c to f(v) in BOXc(H) . This then trivially reflects ! -box containment and is monic,since f is. It also trivially respects composition.
Applying BOX to every morphism in definition 5.1.2 gives us the following:
Corollary 6.3.4. If GiIjH is a !-graph equation,then so is
BOX(G)BOX(i)BOX(I)BOX(j)BOX(H)
We can now state the inference rule
BoxEGHEBOX(GH)
Theorem 6.3.5. Box is sound. In particular,if for all concrete instances GH of GH ,
E~GH
then for any concrete instance GH of BOXb(GH) ,
E~GH
Proof. By theorem 6.2.13,there is an instantiation S of GH from BOXb(GH) in expansion-normal form,and we can further require that S decomposes into T;U where T is a sequence of EXPb operations,followed by KILLb .
Applying EXPb to BOXb(G) produces the disjoint union of BOXb(G) and G . The next EXPb adds another copy of G ,and so on. Finally, KILLb removes the copy of BOXb(G) ,leaving zero or more disjoint copies of G . So applying T to GH will produce GnHn ,where Gn is n disjoint copies of G and Hn is n disjoint copies of H .
Now if we apply U to GnHn ,we know that each operation can only affect a single copy of G in Gn and the corresponding copy of H in Hn . There are thus instantiations U1,,Un of GH such that U(Gn) is U1(G)Un(G) and similarly for U(Hn) (where we are using the notation from remark 4.4.2).
We can then use the assumption to construct proofs of E~Ui(GH) for each 1in ,and use LEIBNIZ to apply these to the decomposed parts of U(GnHn) .
This is mostly useful in the construction of larger proofs. We will demonstrate its use in section [6.4.1]

6.4 !-box Induction

In this section, we introduce an analogue of induction for !-graphs. This will follow the usual induction scheme of having a base case and a step case that must be proved for a particular ! -vertex b . However,in the absence of the named variables of terms,we need some way to link a !-vertex in the inductive hypothesis to one in the equation we need to prove for the step case.
We will introduce the possibility of fixing a !-vertex, which prevents any !-box operations being performed on it during the matching process. The idea is that if we take the following graph
and fix b ,it should match itself and
but not
\chi 5\chi 5
or
as it normally would. The result of this is that, given a rule like where b is fixed,the only possible rewrites are ones like
where the !-box operations that can subsequently be performed on b and c (and hence the possible concrete instantiations) are linked.
In order to deal with multiple applications of the induction rule, we will tag these fixed !-vertices with arbitrary symbols drawn from a (countable) set A . So we could tag b above with xA ; in this case,we say that b is x -fixed,and we only allow b to match c in
if c is also x -fixed.
To store this information,we augment a !-graph G with a partial map
fixG:!(G)A
that maps each fixed ! -vertex to its tag. We require ! -graph morphisms to preserve these tags,and the morphisms of a !-graph equation to also reflect them. In particular, if we have the !-graph equation GH ,the fact we can consider the !-vertices of G and H to be the same means we can view fixG as being the same as fixH ,and call these fixGH .
This will have an impact on the !-graph logic, and the notion of soundness we are considering. Specifically,we will consider what we mean for EGH to hold. Let A=im(fixGH) . For each xA ,each non-negative integer nN0 ,and each ! -graph equation LR ,we define Xnx(LR) to be LR with nEXPb operations and one KILLb operation applied to it for each x -fixed !-vertex b in the equation. Then for each function λN0A from A to the non-negative integers,we define Xλ(LR) to be LR with Xλ(x)x applied to it for each xA (the order is irrelevant,as these are all top-level ! -vertices). Then the semantics of EGH is that for each λN0A and each instance GH of Xλ(GH) ,if we let
Eλ={Xλ(LR)LRE.LRhas nox-fixed !-vertices forxA}
then
E~λGH
in the equational logic of string graphs.
We need to adjust the !-graph logic and rewriting to keep it sound under these modified semantics. We place a side constraint on COPY, DROP and KILL that the !-vertex they operate on cannot be fixed (hence the term "fixed"), and on Box that the equation contains no fixed !-vertices. Likewise, when rewriting, we do not allow any !-box operations to be applied to fixed !-vertices.
Our previous requirement that morphisms preserve fixing tags means that the matching morphisms of a !-graph rewrite can only map x -fixed !-vertices to other x -fixed !-vertices (although an unfixed !-vertex may match an x -fixed one). This also constrains the LEIBNIZ rule.
We also introduce a !-box operation FIXbx(G) that produces a !-graph identical to G but where the ! -vertex b is x -fixed (and similarly for ! -graph equations),and a rule
(FIX)EGi,jHEFIXbx(Gi,jH)
with the condition that b is a top-level ! -vertex of Gi,jH that is not fixed.
In the pictoral representations of ! -graphs,we will mark x -fixed ! -vertices with the label Fx .
The following is the inference rule for ! -box induction,based on one originally suggested as a possibility by Kissinger in his thesis ([23],pp 179-181). It holds providing b is a top-level,unfixed !-vertex in GH and x is a fresh tag (that does not already occur in GH or any of the equations in E ).
(INDUCT)EKILLb(GH)E{FIXbx(GH)}FIXbx(EXPb(GH))EGH
Theorem 6.4.1. INDUCT is sound.
Proof. Let A=im(fixGH) . We need to show that for each λN0A and each concrete instance GH of Xλ(GH),
E~λGH
in the equational theory of string graphs.
We can choose an instantiation of GH in expansion-normal form with all the operations on b at the start (since b is top-level). Denote this T;U ,where T contains all the operations on b ,and U all the other operations. T is comprised of n expansions,for some n ,followed by KILLb .
We show by induction on n that,for all concrete instances GVHV of Xλ(GH) with an instantiation of the form T;V ,
E~λGVHV
n=0:T is just KILLb . It follows from the definition of Xλ that there is an instantiation W of Xλ(GH) from GH such that W only operates on top-level ! -vertices of GH . Then W;T;V is equivalent to T;W;V ,and so GVHV is an instance of KILLb(GH) . The assumption EKILLb(GH) then gives us that
Eλ~GVHV
n=k+1 : let T be T with the first expansion removed (so T=EXPb;T ). We know that T is equivalent to Xkx ,and so V is an instantiation of GVHV from Xkx(EXPb(Xλ(GH))) . But
Xkx(EXPb(Xλ(GH)))=Xλ(Xkx(EXPb(GH)))
since all the operations are on top-level ! -vertices of GH . Further,we can define
μ(y)={λ(y)yAkx=y
and then
Xλ(Xkx(EXPb(GH)))=Xμ(FIXb(EXPb(GH)))
So now we have that V is an instantiation of GVHV from Xμ(FIXb(EXPb(GH))) ,and then the step case assumption means we can construct a proof of
E~μGVHV
Now the way μ was defined means that
Eμ=Eλ{Xλ(Xkx(GH))}
and so the proof may contain invocations of AXIOM with a concrete instance of Xλ(Xkx(GH)) . Consider one such invocation,where the axiom GWHW is a (concrete) instance of Xλ(Xkx(GH)) , which is the same as Xkx(Xλ(GH)) . Then GWHW is an instance of Xλ(GH) and there is an instantiation of the form T;W witnessing this. The inductive hypothesis then allows us to construct a proof of
E~λGWHW
We can thus replace all such AxIOM invocations with proof trees using only the axioms of Eλ ,and so discard Xλ(Xkx(GH)) from Eμ ,leaving us with a proof of
E~λGVHV
as required, and the induction is complete.
Now we just let V=U ,and we have
E~λGH
as required.
This can be viewed as a sort of ! -box introduction rule,more powerful than Box (although relying on correspondingly stronger assumptions). It can be used to produce !-versions of concrete equations, such as those generated by an automated tool like QuantoCosy 23.
Example 6.4.2. Suppose we have the following three graph equations,drawn from the Z/X calculus presented in section 2.2(6.2) (6.3) (6.4)
The first two are easily found by QuantoCosy, and the latter is the spider theorem arising from commutative Frobenius algebras. We wish to use !-box induction to show(6.5)
The base case is just (6.2), and so is trivially satisfied. Now we need to show that adding
to the other equations allows us to derive
This follows using !-graph rewriting:

6.4.1 The Generalised Bialgebra Law

We now demonstrate a more ambitious application of ! -box induction,where we derive the generalised bialgebra law for the Z/X calculus
Recall the axioms of the Z/X calculus:
We have omitted the commutativity laws, as these are inherent in the fact that all the nodes are variable-arity,and hence the inputs (resp. outputs) of a Z or X node are indistinguishable from each other. In particular,
[8]1
is actually the same string graph equation as DUAL.
We will start by proving some symmetries of these equations. Note that, for brevity, we will tend to condense multiple applications of the same rewrite rule (or of rules that differ only by colour).
Lemma 6.4.3.
(6.6)[8]1
Proof.
Lemma 6.4.4.(6.7)
We have already derived(6.8)
and(6.9)
follows from (6.7) by essentially the same proof.
Lemma 6.4.5.(6.10)
Proof. Proof by INDUCT on b . The base case is and the inductive step is(6.11) (6.12)and on XSP to get(6.13)
Lemma 6.4.6.
Proof. Proof by INDUCT on b . The base case is
Theorem 6.4.7.
Proof. First we use Box on ZSP to get
We will need to use INDUCT twice. First,we use it on b1 . The base case is The inductive hypothesis is(6.14)
and we need to show
(6.15)
We apply INDUCT again,this time on b2 . The base case is
The new inductive hypothesis is
(6.16)and we need to show
(6.17)
Thus we have demonstrated that (6.17) holds, so INDUCT gives us that (6.15) holds, and INDUCT again gives us that the theorem holds.
This example, while a demonstration of the power of INDUCT, still requires the rewrite system to initially contain the spider laws. Appendix B demonstrates a possible way of using !-box induction to introduce !-boxes into rewrite systems that previously contained only concrete rewrite rules.

6.5 Merging !-boxes

The MERGE operation presented in this section was included as one of the core !-box operations in
[26] (pp 6-7,10-11). Theorem 6.5.5 demonstrates that this is unnecessary.
Suppose we have the equation
and the graph
It is easy to see that for any concrete instance of the graph, there will be a concrete instance of the equation whose LHS matches the graph: we just need to do the same things to both b and c that we do to d . However,the LHS of the equation as it stands will not match the graph.
In order to allow this, we will introduce a new !-box operation that will merge two disjoint !-boxes in a !-graph. The two !-boxes will need to have the same parents in order to ensure that combining them will not affect the contents of any other ! -box in the graph.
Definition 6.5.1 (MERGE; [26],pp 7). Suppose G is a !-graph and b,c!(G) ,with B(b)b= B(c)c and B(b)B(c)={} ,then MERGEb,c(G) is a quotient of G where B(b) and B(c) are identified. More explicitly, this is the coequaliser
(6.18)B(b)c^b^GMERGEb,c(G)
in Graph/GT! where b^ is the normal inclusion map and c^ is the inclusion of B(c) into G composed with the obvious isomorphism from B(b) to B(c) .
This construction identifies b and c ,and leaves all the other vertices of G untouched. The preconditions ensure that every incoming edge of b corresponds exactly to an incoming edge of c (and vice versa); each such edge to b is identified with its corresponding edge to c . If a pair of !-vertices satisfy the preconditions of MERGE, we say they are mergable.
Proposition 6.5.2. Let G be a ! -graph with mergable ! -vertices b and c . Then MERGEb,c(G) is a !-graph and U(G)U(MERGEb,c(G)) .
Proof. Let H=MERGEb,c(G) ,and let h be the coequaliser map.
B(b)c^b^GhH
H exists in Graph/GT! ,as Graph/GT! has coequalisers of monomorphisms. Note that h is surjective by lemma 4.2.7 since it is a regular,and hence strong,epimorphism of Graph/GT! .
We can construct a morphism f:GBOX(U(G)) that is the identity on U(G) (and collapses all the other !-boxes),and this trivially coequalises b^ and c^ . So there is a unique g making
commute. Since U(f) is an isomorphism, U(h) is a (split) monomorphism as well as being a strong epimorphism,and hence is invertible. So U(G)U(H) and hence U(H) must be a string graph, since U(G) is.
Let x,y be vertices in !(G) such that h(x)=h(y) . We can show that either x=y or {x,y}= {b,c} . Suppose xy ,let G be U(G) together with the graph of ! -vertices
and edges from a and b to each vertex of U(G) . Then let f:GG be the identity on U(G) and take every vertex in !(G) to a except y ,which it takes to b . This also fixes the edge maps. If yb and yc,g will coequalise b^ and c^ ,and so there must be a unique map g:HG such that f=gh . But then g(h(x))g(h(y)) even though h(x)=h(y) ,which is impossible. So we must have y=b or y=c . Repeating with the roles of x and y switched,we get that x=b or x=c . Thus if xy ,then {x,y}={b,c} .
β(H) is reflexive as it is the image of β(h) ,the domain of which is reflexive.
Let xy be vertices in β(H) with e1,e2 edges between them such that s(e1)=t(e2)=x and t(e1)=s(e2)=y.
β(G) is anti-symmetric,and so the preimages of e1 and e2 in under h cannot be in the same loop construction. Thus either x or y must be mapped to by more than one vertex of G ,and hence must have the preimage {b,c} . This cannot be true of both,since xy . WLOG,suppose it is true of x . Then y ,the preimage of y ,must be in B(b) and B(c) (or vice versa). But B(b)b=B(c)c and (since yc ) y must be in B(b) ,which can only be true if y=b ,which we assumed was not the case. So there can be no such e1 and e2 .
Simplicity of β(H) follows a similar argument: if e1 and e2 are edges from x to y where xy , then if the preimage of y is {b,c},x must be in the image of b^ and c^ and so the preimages of e1 and e2 must be coequalised by h and hence e1=e2 ,and if the preimage of x is {b,c} then the fact that B(b)B(c)= means the preimages of e1 and e2 must be the same,and hence e1=e2 .
For transitivity,let x,y,z be vertices in β(H) with e1 an edge from x to y and e2 from y to z . Let e1,e2 be arbitrary preimages of the respective edges under h ,as before. Then either t(e1)=s(e2) ,in which case the existence of an edge from x to z is immediate from transitivity of G ,or {t(e1),s(e2)}={b,c} . WLOG,assume t(e1)=b and s(e2)=c . Then B(b)b=B(c)c gives us that s(e1) must be a predecessor of c ,and so x must be a predecessor of z ,as required.
Let d!(H) . Then,because h is surjective and U(h) is bijective, U(B(d)) is the union of U(h)[U(B(d))] for each preimage d of d under h . But U(h) is an isomorphism,so U(B(d)) is the union of open subgraphs of U(H) ,and hence is open in U(H) .
For the final requirement of a !-graph,suppose d,d!(H) with dB(d) . We need to show,for any vertex v of H with vB(d) ,that vB(d) . If v is a !-vertex,this follows from transitivity of β(H) . Otherwise,the edge e from d to v has a preimage e0 under h ,as does the edge e from d to d . If t(e0)=s(e0) ,there must be an edge from s(e0) to t(e0) in G ,which will map to an edge from d to v in H . Otherwise,we must have t(e0)=b and s(e0)=c (or vice versa,which is equivalent). But then the preconditions for MERGE require an edge from s(e0) to c as well,which also induces an edge from s(e0) to t(e0) ,and hence from d to v .
Proposition 6.5.3. Let f:GH be a morphism of BGraphT that reflects ! -box containment, and let b and c be mergable ! -vertices of G such that f(b) and f(c) are mergable in H . Then there is a unique morphism
MERGEf(b),f(c)(f):MERGEb,c(G)MERGEf(b),f(c)(H)
making the following diagram commute
where the down arrows are the coequaliser maps from the definition of MERGE, and this morphism reflects ! -box containment. Further,this construction preserves monomorphisms and strong epimorphisms and respects composition.
Proof. Let G=MERGEb,c(G) and H=MERGEf(b),f(c)(H) . We will construct the following commuting diagram
where f will be uniquely determined by universality of coequalisers. This will then be MERGEf(b),f(c)(f) .
The top square is two separately-commuting squares: fb^=f(b)^fb and fc^=f(c)^fb . If d is a vertex in B(b) ,then the edge witnessing this is mapped by f to one witnessing f(d)B(f(b)) . So if we let fb be fb^ ,the restriction of f to B(b) ,reinterpreted with codomain B(f(b)) then we have the first commuting square. The second follows from the fact that B(b)b=B(c)c and similarly for f(b) and f(c) .
Now h coequalises f(b)^fb and f(c)^fb ,and hence coequalises fb^ and fc^ . So hf coequalises b^ and c^ . Then universality of g means that there is a unique f making the bottom square of the diagram commute. This universality also means that MERGE respects composition.
The fact that f reflects ! -box containment means that fb is surjective,and hence epic. Then if we have morphisms a:GK and b:HK such that ag=bf ,we know
agb^=agc^
bf(b)^fb=bf(c)^fb
bf(b)^=bf(c)^
Then,since b equalises f(b)^ and f(c)^ ,there is a unique arrow k:HK such that b=kh . Since g is epic,we also have a=kf ,and hence the bottom square of the diagram is a pushout. BGraphT preserves monomorphisms under pushouts,and hence f is monic whenever f is. Also,if f is strongly epic,and hence surjective,the same must be true of hf and hence of fg . So f is surjective, and hence strongly epic. Since it is surjective, it trivially reflects !-box containment.
Since U(G)U(MERGE(G)) for ! -graphs, U(f) is the same as U(MERGE(f)) (up to isomorphism) and so we can simply apply MERGE to the morphisms of definition 5.1.2 to get the following:
Corollary 6.5.4 ([26],pp 10-11). Let LiIjR be a !-graph equation,and let b,c be mergable !-vertices of I . Then
MERGEi(b),i(c)(L)MERGEi(b),i(c)(i)MERGEb,c(I)MERGEj(b),j(c)(j)MERGEj(b),j(c)(R)
is also a !-graph equation.
In the case that b and c are mergable ! -vertices of GH ,we posit the following rule:
 MERGE EGHEMERGEb,c(GH)
Theorem 6.5.5. MerGE is sound.
Proof. We will show that every concrete instance GH of MERGEb,c(GH) is also a concrete instance of GH . Suppose S is a concrete instantiation of GH from MERGEb,c(GH) in expansion-normal form.
While instantiations may only contain COPY, DROP or KILL operations (EXP being a composite of these), for the purposes of this argument we will relax this to allow MERGE operations as well. This is purely a convenience to allow us to call our intermediate steps "instantiations" before we finally arrive at a genuine instantiation containing only those three operations. So we start with the "instantiation" MERGEb,c;S of GH from GH ,and transform it into a genuine instantiation with no MERGE operations.
The intermediate instantiations may have multiple MERGE operations, but we will always keep these together,and they will not interfere with each other: if H=MERGEb,c(G) and K=MERGEb,c(H) are two adjacent operations in the instantiation,where GgHhK are the coequaliser maps,we will have that bB(g(b)) and g(b)B(b) ,and similarly h(g(b)) will not interfere with the !-vertices acted on by any MERGE operation on K and so on. This allows us to freely reorder the MERGE operations.
We will use this to collate them into a "composite" MERGE that simultaneously operates on multiple pairs of mergable ! -vertices,where each pair has distinct parents to any other pair. We will only ever have one such operation in the sequence; initially, it will be at the start and will have a single pair, b,c . When it has no pairs,there are no MERGE operations left in the sequence and we are done.
We will move the MERGE right one operation at a time until the set of pairs it operates on is empty. So consider the operation to its right. This is either KILLd or EXPd for some ! -vertex d.d cannot be a child ! -vertex of any of the merged vertices,since d must be a top-level ! -vertex. If none of the merged vertices are in B(d) ,the operations are independent,and we can move the MERGE one place to the right without changing the resulting graph.
Suppose the operation is KILLd . If d is a merged vertex,call its preimages under the co-equaliser d0 and d1 . If we remove the KILLd ,remove the pair d0,d1 from the MERGE and put KILLd0;KILLd1 before the MERGE,we will get the same graph. Otherwise,suppose d is not a merged vertex,but B(d) contains a merged vertex. Then we can swap KILLd with the MERGE and remove any pairs in B(d) from the MERGE.
Suppose instead the operation is EXPd . If d is a merged vertex,we can remove EXPd and put EXPd0;EXPd1 before the MERGE,leaving the set of merged vertices untouched. Otherwise, suppose d is not a merged vertex but B(d) contains one,and say it results from the pair x,y . Then we can swap EXPd and the MERGE,providing we add x,y to the set of merged vertices,where x is the copy of x under the expansion and y is the copy of y.x and y have no edges to or from x and y ,or the !-vertices of any other merged pair. If there are any other such pairs,do the same to them as well.
Since the number of operations to the right of the MERGE always decreases, this will eventually terminate,and we will have a concrete of instantiation of GH from GH .

6.6 A More Traditional Logic

Those familiar with formal logics will have noticed something strange about the one presented at the start of this chapter,as well as the one in section 3.5 the equality predicate is not really a predicate at all. What we have presented is a logic of "string graph equations" and "!-graph equations", where those "equations" are actually spans in a category.
In this section, we will sketch out an equational logic of !-graphs, where the equality predicate is just a formal symbol indicating that the objects on either side of it should be considered equal. As we noted in section 3.4.1, we need to somehow encode the correlation between boundaries of string graphs; we also need to encode the correlation between !-vertices in both graphs. !-graph equations are one way of doing this, but to get a more traditional equality predicate, we will extend the idea of a framed cospan (definition 3.4.1) to ! -vertices.
Definition 6.6.1 (!-Framed Cospan). A !-graph frame is a triple (X,<,sgn) where X is a !-graph consisting only of isolated wire-vertices,!-vertices and edges whose sources are !-vertices; < is a total order on VX ,the vertices of X ; and sgn:VU(X){+,} is the signing map.
A cospan of ! -graph monomorphisms XdGcY is called a ! -framed cospan if
  1. X and Y are !-graph frames
  1. G contains no isolated wire-vertices
  1. the following is a pushout square:
  1. for every vVU(X),d(v)In(G)sgn(v)=+
  1. for every vVU(Y),c(v)Out(G)sgn(v)=+
As with the framed cospans of string graphs, we can frame a !-graph equation:
Definition 6.6.2. A framing of a !-graph equation Li1,i2R is a pair of !-framed cospans Xa LbY and XcRdY such that there are morphisms j1 and j2 forming the coproduct (ie: disjoint union) Xj1Ij2Y and making the following diagram commute:
Just as with framings of !-graph equation, such a framing is equivalent to a !-graph equation, in the sense that any !-graph equation can be framed, and the !-graph equation can be recovered from the two !-framed cospans. If two !-framed cospans have isomorphic left and right (or domain and codomain) !-graph frames, they induce a !-graph equation, and we call them compatible.
With this is mind, we can construct a logic of !-framed cospans that is equivalent to the logic presented in this chapter. We have a choice in how we represent the set of axioms: we can use a set of !-graph equations and the rule
(Axiom)Gi,jHEEG^H^
where (G^,H^) is a framing of Gi,jH ,or we can use a set of pairs of compatible !-framed cospans and have the rule
(Axiom)(G^,H^)EEG^H^
The equivalence relation rules are simple:
(Reft) EG^G^ (Sym) EG^H^EH^G^ (Trans) EG^H^EH^K^EG^K^
For the others, we will need to introduce some new notation, or at least extend existing notation. For example,if f:GH is a wire homeomorphism of !-graphs,and G^=XGY is a framed cospan,then there is a framed cospan H^=XHY where the inclusions of the framed cospans commute with f! and fB . We can then view f as a wire homeomorphism from G^ to H^ .
HOMEO can then be expressed as
(HOMEO)EG^H^EG^f(H^)
where f is a wire homeomorphism (note that the presence of SYM means that this is equivalent to the version of HOMEO on !-graph equations).
LEIBNIZ requires a bit more work. We will borrow the notion of contexts from term-rewriting, where they are terms with "holes" in them: placeholders that can be substituted with other terms to produce a valid term overall.
The idea with !-graphs will be to provide both an "external" interface to the graph, as a !-framed cospan does, and an "internal" interface. An simple example (without any !-boxes) would be
We could then take a !-framed cospan whose frames match the internal interface of the context, such as
and embed it in the context by merging the images of the frames producing the !-framed cospan
When there are !-vertices to account for, the !-graph frames of the external interface must contain all the !-vertices (and edges between them) in order for the final construction to be a !-framed cospan. The internal interface need not contain all the !-vertices of the graph, though.
Definition 6.6.3. A ! -graph context C is a pair of ! -graph cospans
XIdIGcIYI
XOdOGcOYO
where
  • G contains no isolated wire-vertices
  • XI,XO,YI and YO are !-graph frames
  • β(XI)β(YI)
  • β(XO)β(YO)β(G)
  • the morphisms are all monic and reflect !-box containment
  • Bound (U(G)) is the disjoint union of the images of U(dI),U(cI),U(dO) and U(cO)
  • for every vVU(XI),dI(v)In(G)sgn(v)=+ ,and similarly for dO
  • for every vVU(YI),cI(v)Out(G)sgn(v)=+ ,and similarly for cO
Given such a !-graph context and another !-framed cospan
H^=YIdIHcIXI
we can merge the context with H^ (we say that C accepts H^ ). We first merge G and H ,using YI as the overlap, in a manner similar to the composition of framed cospans from section 3.4.1
K is a !-graph by a similar argument to the one that shows composition of framed cospans to be well-defined (note the reversal of the frames for H^ means that the interpretation of the signing map on the frames is reversed,so inputs of H will be merged with outputs of G and vice versa).
Next,we merge the two images of XI using the following coequaliser:
XIi2cIi1dIKfG+H
Then we define C[H^] to be the framed cospan
XOfi1dOG+Hfi1cOYO
Now we can write LEIBNIZ as
(LEIBNIZ)EG^H^EC[G^]C[H^]
where C is a !-graph context that accepts G^ and H^ (note that the compatibility of G^ and H^ means that if C accepts one then it must accept the other).
In this version of LEIBNIZ,the context graph takes the place of D in the !-graph rewrite
and the internal frames (XI and YI) take the place of I .
The final piece of this logic of ! -graph frames is the ! -box operations. We extend them to ! -graph cospans in the same way that we extended them to !-graph equations: if
G^=XdGcY
then
OP(G^)=OP(X)OP(d)OP(G)OP(c)OP(Y)
Now we can write, for example,
(COPY)EG^H^ECOPYb(G^)COPYb(H^)
(since the compatibility of G^ and H^ means that we consider b to be in both if it is in either),and similarly for the other !-box operation rules.
Thus we have a logic with a normal equality predicate based on !-framed cospans. What is more, by considering only concrete graphs, the same construction can be used to produce a logic based on framed cospans from the logic presented in section 3.5 .
In practice, a theorem prover would probably use names to store the equivalent of the !-graph frames; the signing maps and the division between the domain and codomain are not particularly important for the construction of proofs (as can be seen from the fact that the !-graph equation structures do not store this information).

Chapter 7

Computability of ! -Graph Matching

Suppose we have a !-graph (or string graph) G and a !-graph rewrite rule LR that we wish to use to rewrite G ; as previously stated,we want rewriting to be up to wire homeomorphism. If we can find a rewrite rule LR that is wire-homeomorphic to an instance of LR such that there is a local isomorphism m:LG that reflects ! -box containment,theorem 5.3.3 tells us that the rewrite(7.1)
exists. In fact,it is easy to find this rewrite: if we remove from G the image of everything in the interior of L (ie: the image of everything in L that is not in the image of i ),we get D;g is the subgraph relation and d is a restriction of m.H ,being a pushout of monomorphisms,is just a graph union. In a practical implementation, where vertices and edges are likely to be named components, the main difficulty is managing the names to make sure there are no clashes when building H .
That still leaves finding suitable instances, finding suitable rules wire homeomorphic to those instances and finding a local isomorphism that reflects !-box containment. Section 3.6.2 discussed the latter two (except reflecting !-box containment, which can be implemented by filtering the results); in this chapter,we will demonstrate that,providing LR is "well behaved" in terms of the instances it can produce, we can finitely enumerate all instances of the rule that can result in a matching onto a particular G . We will also describe how Quantomatic implements these steps.

7.1 Enumerating Instances

In order to find all possible matchings,we need a way of searching the space of graphs H such that GH ; while this space will almost always be infinite,it will usually be the case that only a finite number of them will be candidates for matchings.
Suppose we wish to match a !-graph G onto another !-graph H ; we need to find an instance G of G and a monomorphism from G to H (or,rather,from a graph wire homeomorphic to G to a graph wire homeomorphic to H ). The monomorphism must satisfy additional constraints (definition 5.3.2), but these are not important to this discussion.
As long as G has any (unfixed) !-vertices,it will have an infinite number of instances (to see this, consider repeatedly applying COPY to one of the !-vertices). However, in most cases, only a finite number of these will have a monomorphism to H .
In particular,we can safely ignore any instance of G that has more node-vertices,circles or fixed ! -vertices than H ,as the number of each of these is constant under wire homeomorphism. We cannot, however, restrict the search based on the number of wire-vertices. Consider, for example, the following pattern and target graphs:
No matter how many times the !-box in the pattern is expanded, we can always introduce enough wire-vertices in the target graph's wire to accommodate them all. So there are an infinite number of matchings in this case. Empty !-boxes do not even need a wire in the target graph to exhibit this behaviour.
We call these (unfixed) !-boxes, containing no node-vertices or circles, wild !-boxes. In order for it to be possible to enumerate all candidate instances of G ,we will require that no instance of G contains any wild ! -boxes. To show this for any given G ,it is sufficient to show that for each b!(G) , B(b) is not wild after killing all ! -vertices not in B(b) . The rest of this discussion will assume no instance of G contains wild !-boxes.
The first step is to consider how to explore the space of instances in an ordered way. There may be an infinite number of witnesses of even a single instance,since applying COPYb;KILLb1 to a graph G with a !-vertex b yields a graph isomorphic to G ,and so we cannot simply try to build every possible instantiation. At the same time, we cannot depend on expansion-normal form as we need to deal with arbitrary instances, not just concrete ones.
That said, we can produce something similar enough to expansion-normal form for our purposes. We will use the FIX operation used in section 6.4, and we will adjust our definition of depth to ignore !-vertices that have been fixed (so a !-vertex with only fixed parents has depth 0). Since we are really using this as a notational convenience, we will relax the constraints on FIX to allow the fixing of ! -vertices whose parents are all fixed. The important thing to note is that,in the context of instantiations,FIX behaves just like DROP: after FIXbx ,there can be no further operations on b , and it can potentially reduce the depth of any children of b .
If we take an instantiation S of G from G and a fresh fixing tag x ,and append a FIXbx operation for every b!(G) ,then the result,call it S ,is enough like a concrete instantiation for the arguments from section 6.2 to hold with minimal adjustment (just read "FIX" or DROP" wherever DROP is mentioned). We also need an equivalent of EXPb ; we will call this CFIXbx ,which will be a shorthand for COPYb;FIXb1x .
So we can transform S into a witness for GG that is depth-ordered (according to our revised definition of depth) and is composed entirely of EXP,KILL and CFIXx operations. As a result,we only need to search for instantiations of this form in order to find all possible instances.
Remark 7.1.1. Using this trick comes with a caveat: when we attempt to find a morphism from G to H ,an x -fixed ! -vertex would ordinarily only be allowed to match another x -fixed vertex. However,we want x -fixed vertices to behave like unfixed vertices when it comes to building matching morphisms, and allow them to match any vertex of the target graph. This can be acheived by either removing all x -fixing tags from G before finding the matching morphism (which is the approach taken by the algorithm in section 7.2) or by relaxing the constraint with a special case for the x tag.
We will call the area of the pattern graph not in any !-boxes or only in fixed !-boxes the match surface. This is the graph that would result from killing all the unfixed !-boxes. Importantly, no EXP,KILL or CFIXx operation can reduce the match surface. Furthermore,if every !-box of every instance of G contains at least one node-vertex or circle,EXP and CFIXx must always increase the number of node-vertices or circles in the match surface.
We will take an inductive approach to finding instances of G that are candidates for a matching onto H ,starting with the zero-length instantiation. To build the instantiations of length n+1 , for each instantiation S of length n (resulting in a !-graph GS ) and each unfixed b!(GS) with depth 0,we will create three new instantiations by appending KILLb,EXPb and CFIXbx to S . If the resulting graph has more node-vertices, circles or fixed !-vertices in its match surface than are in H ,we will discard that instantiation (and hence not consider it as a prefix for the instantiations of length n+2 ).
Remark 7.1.2. Note that there are more efficient versions of the algorithm; for example, it is sufficient to choose an arbitrary depth 0 !-vertex at each stage rather than generating new instantiations for each such ! -vertex. However,it is easier to see that the algorithm here is correct,and this version suffices to show computability.
It should be clear, given the preceeding discussion, that the algorithm will enumerate all instances of G that have a monomorphism to H . It remains for us to show that it will terminate,providing every ! -box of every instance of G contains at least one node-vertex or circle.
Let xH be the number of node-vertices in H and yH the number of circles. Suppose S is an instantiation produced by the algorithm at some iteration step,and let xS and yS be the corresponding properties for the match surface of GS . Every EXP and CFIXx operation must increment either xS or yS (and KILL cannot decrease either),and the algorithm will discard any instantiation where
xS+yS>xH+yH
So there can be at most xH+yH EXP or CFIXx operations in S .
Each of these operations can, at most, double the number of unfixed !-vertices in the graph, and KILL can only reduce that number. Thus if zG=|!(G)|,S cannot contain more than zG2xH+yH KILL operations. |S| ,the length of S ,is therefore bounded by
xH+yH+zG2xH+yH
which is a finite number fixed by G and H .
The same bound also places a limit on |!(GS)| ,limiting the number of ways S can be extended. The total number of steps in the algorithm is then bounded, and hence it terminates.
Note that this approach encompasses rewriting both string graphs and !-graphs with !-graph rewrite rules; the former is simply a special case of the latter,without any CFIXx operations.

7.2 Matching in Quantomatic

Quantomatic interleaves the three steps of !-graph matching (instantiation, wire homeomorphism and building a suitable morphism) in a branching algorithm. In this section, we will describe this approach. We will start with the algorithm as currently implemented, which assumes the target graph has no ! -vertices,and then describe how we plan to extend it to allow arbitrary ! -graphs as the target.
The algorithm maintains a partial graph monomorphism from the pattern graph to the (concrete) target graph. It terminates when this is a complete morphism, and is successful if it is a local isomorphism.
The overall approach is to extend the graph morphism to the match surface (those parts of the pattern graph not contained in any unfixed !-boxes), then choose a top-level !-vertex and try killing it or expanding it. In the expansion branch, the match surface will have increased, so we repeat the graph morphism extension step,before trying another ! -vertex. In the killing branch,we proceed straight to choosing another ! -vertex. At each choice that could affect the final match,the algorithm branches, so as to explore all options. If it fails to extend the graph morphism to the match surface at any point, that branch terminates with failure.
Circles are matched first in each round of extending the graph morphism. Circle matching involves taking each unmatched circle in UC and matching it to an arbitrary unmatched circle of the same type in T ,and removing the vertex from T . Since circles are indistinguishable under rewriting (being wire-homeomorphic to each other), no branching needs to occur. Doing this first therefore reduces the amount of work duplicated across branches of the algorithm.
Figure 7.1: !-graph matching onto string graphs
Figure 7.2: String graph matching subroutine
Bare wires are left until the very end of the matching process, after all the instantiation has been done. This is because (as noted in the discussion on wild !-boxes) bare wire matching does little to constrain the possible instantiations and can generate a lot of branches. For each bare wire set in the match surface,the bare wire matching step branches for each unmatched edge e in G connected to a wire-vertex of the same type as the bare wire. It then replaces e with three edges and two wire-vertices (of the appropriate type):
and matches set to the new wire-vertices and the edge between them.
To deal with wire homeomorphism, the algorithm starts with a variant of the normalisation scheme from section 3.6.2 every interior wire has two wire-vertices; bare wires have only the input and output vertices; circles have a single wire-vertex; and input and output wires have only the input or output vertex in the pattern graph but an extra wire-vertex in the target graph. This ensures that a wire that can accept a match from a bare wire (ie: any wire other than an interior wire already matched by an interior wire or a circle matched by a circle) always has at least one unmatched edge when the bare wire matching step is reached.
During a run of the algorithm to match a !-graph L onto a string graph G ,Quantomatic maintains the following state:
  • L : a normalised (as described above) !-graph
  • L : an instance of L
  • S : a partial instantiation of L ,resulting in L
  • G : a normalised (as described above) string graph
  • m:VLVG : a partial injective function describing the matching so far
  • UVL : a set of unmatched vertices of L
  • PN(L) : a set of partially-matched node-vertices
  • PSP : a set of scheduled partially-matched node-vertices
  • TVG : a set of vertices that can be matched onto
Note that we do not maintain a map of edges; this is because !-graphs are simple, so if a function from vertices of one graph to vertices of another extends to a graph morphism, it does so uniquely.
U is partitioned into UC ,containing wire-vertices in circles (of which there can only be one for each circle), UW ,containing other wire-vertices,and UN ,containing node-vertices.
A note on terminology: a vertex is matched if it is in either the domain or image of m . If n is a matched node-vertex of L ,we call it (and its image m(n) ) partially matched if some of the neighbourhood of m(n) is not in the image of m . Otherwise,it is completely matched. The same terminology applies to m(n) . For example,consider the following incomplete matching:
n has been matched to a vertex in the target graph,but we will need to expand the !-box twice before we are done with n . This is an example of a partially matched node-vertex.
P is (a superset of) the set of partially matched vertices of L ,and PS is intended to contain those node-vertices of P that may be able to become completely matched due to the application of a !-box operation.
We split the algorithm description into two parts. Figure 7.1 contains the part of the algorithm that explores the instantiation space, and figure 7.2 has the part that extends the match morphism. This latter part can be used in a simpler wrapper to match string graphs onto string graphs.
Red wires (with labels starting "each") indicate a branching point. A branch is created for each possibility. If there are no possibilities, the current branch dies. So, for example, if the algorithm takes a vertex from UN and there are no possible matchings for it in the target graph,that branch will be killed off.
The initial match state has L=L and G normalised (in the manner described above), S=m= U=P=PS= ,and T populated with all the vertices of G not in bare wires.
A proof of the correctness of this algorithm can be found in appendix A

7.2.1 Matching Onto !-Graphs

In this section, we describe how the previous algorithm can be extended to match arbitrary !-graphs. This algorithm has been implemented for Quantomatic (albeit not in a released version yet).
Firstly, we need to maintain information about which !-vertices are fixed. Since !-vertices are only fixed at intermediate stages of a proof (when using INDUCT or during the matching process itself), we maintain the information about which !-vertices are fixed with which tags separately to the graphs. Thus we extend the match state (and algorithm inputs) with two partial maps, FL:!(L)A and FG:!(G)A.
We also add two further sets to the match state to keep track of !-vertices:
  • BSdom(FL) : a set of unmatched fixed !-vertices
  • BC!(L) : a set of ! -vertices that can be copied
Figure 7.3: !-graph matching onto !-graphs
Figure 7.4: !-box matching subroutine
  • BE!(L) : a set of !-vertices that can be expanded
The initial match state is mostly empty as before,with G and L=L again normalised. We also populate U with the vertices of L that are not in any !-box,and T with all the vertices of G that are not in any ! -box. The new parts of the match state are populated as follows:
-BS=dom(FL)
-BC={b!(L)BS:δ(b)=0}
-BE=
The string graph matching subroutine is extended (via "hooks" in the implementation) to allow the matching to be constrained by !-box membership. In particular,we only allow a vertex vVL to match a vertex vVG if m[Bv]=Bv ,where Bv={b!(L):vB(b)} and Bv={b!(G) : vB(b)}
Also implicit in the algorithm description is that when we kill a !-vertex b ,we always add any vertices in P that were adjacent to B(b) to PS ,so that the next string graph matching run can remove them from P if they are now completely matched.
Additionally,one part of figure 7.4 refers to a "candidate for m(b) ". If b!(L)dom(m) ,we say that b!(G)im(m) is a match candidate for b if
  • it shares the same parents (ie: m[B(b)b]=B(b)b ),and
  • if b is fixed, b is fixed with the same tag (ie: (bdom(FL)FL(b)=FG(b)) )
The major difference between this algorithm and the previously-presented one is that CFIXbx is provided as an alternative choice to EXPb and KILLb when the algorithm deals with the next top-level !-vertex of L .

Chapter 8

Conclusions and Further Work

In this dissertation, we have demonstrated how the string graph formalism for the diagrammatic languages of traced symmetric monoidal categories and compact closed categories can be extended to allow the finitary representation of infinite families of string graphs and string graph equations, and how these !-graphs and !-graph equations can be used in conjunction with double-pushout graph rewriting to do equational reasoning both with and on infinite families of morphisms in these categories. We have also presented some inference rules for a nascent logic of !-graphs.
We started by extending the language of monoidal signatures to allow for nodes with variable-arity edges, representing families of morphisms such as the spiders induced by commutative Frobenius algebras.
We then further extended string graphs with a language, internal to the graph, describing potentially infinite families of string graphs. We extended the notion of string graph equations to these !-graphs, constructing !-graph equations (and rewrite rules) to represent infinite familes of string graph equations (and rewrite rules).
We demonstrated how these !-graph rewrite rules can be used to both rewrite string graphs and to rewrite !-graphs, producing new !-graph rewrite rules. We showed that this rewriting is sound with respect to the interpretation of ! -graphs and ! -graph rewrite rules as families of string graphs and string graph rewrite rules.
We described an equational logic of ! -graphs implemented by ! -graph rewriting and built on this with further inference rules, forming a logic of !-graphs that is again sound with respect to the interpretation of 1 -graphs as families of string graphs. This included a graphical analogue of induction, which we used to derive the spider law for commutative Frobenius algebras.
We rounded off by showing how !-graph rewriting can be implemented. We demonstrated that, providing a !-graph rewrite rule has no instantiations with wild !-boxes, it is possible to determine the finite set of instances of the rule that apply to a given !-graph, and gave an example of an algorithm to find matchings, with their associated instantiations, from the LHS of a !-graph rewrite rule to a string graph or !-graph.

8.1 Further Work

The most obvious next step would be to remove the requirement that variable-arity edges of the same type commute by placing an order on the (variable-arity) edges of a node and using this order when determining the value of the elementary subgraph containing that node. This would allow us to have spiders for non-commutative Frobenius algebras.
A visual way to represent this could be to place a "starting mark" on a node, and count clockwise from there:
Then we would have that the following two graphs are not the same:
ACAC
and, in particular, we would not allow a graph homomorphism from one to the other. The implications of this need working out in detail to ensure there are no unexpected side-effects; for example, there is a potential difference between expanding a !-box clockwise and anti-clockwise. It would allow more expressivity, though, and the commutative version presented in this thesis should be recoverable by placing constraints on the allowed valuations.
Another idea that could be investigated is "defined" generators. For example, suppose we have a commutative monoid (A,,q) . We could define a "spidered" version of this in the following manner:
This essentially defines two !-graph rewrite rules
Some restrictions would need to be placed on such a rewrite system, such as termination and preservation of value, in order for it to be considered a definition, but this could be a powerful tool for proving theorems. Appendix B uses it to prove the spider law for a commutative Frobenius algebra.
The above definition has a major drawback, though, in that it implicitly requires that the monoid is commutative. For example, suppose we have the graph
This can be expanded to
using the rewrite system implied by the definition, but it can also be expanded to
which, in the absense of commutativity and associativity laws, could have a different value. This is because all the incoming edges of the variable-arity multiplication have the same type, and so we have a choice of matches when rewriting.
However, if we combine this idea of definitions with the non-commutative generators already mentioned, we can make the definition
which will produce a unique expansion for each possible starting graph. In particular, it forces the incoming edges to this node to be expanded in clockwise order, so
has the unique expansion
There are undoubtably more inference rules to be discovered. For example,a variant on BOX(G) (section 6.3) that adds a fresh ! -vertex b to G but only adds edges to itself and to vertices in U(G) is likely to give rise to a similar inference rule to Box, but this has yet to be proved sound.
Kissinger introduced a notion of critical pairs for graphs in [22]. The rewriting of !-graphs laid out in this thesis could potentially be used, in combination with Kissinger's definition of critical pairs, to compute confluent extensions to rewrite systems of !-graphs using a Knuth-Bendix completion algorithm[19].
Of course, one of the most important steps to take is to actually implement the ideas presented in this thesis. In particular, we are planning to implement and prove the correctness of the algorithm in section 7.2.1. This algorithm could no doubt be improved, however, to make it more efficient. For example, many graphs involving commutative Frobneius algebras have a lot of internal symmetry, which results in multiple matches being found that all produce the same rewrite; it would be desirable to eliminate this duplication,preferably at the matching stage
The implementation of the ideas in this thesis is work that is currently underway in the Quan-tomatic project [25], which aims to be a useful proof assistant for string diagrams in compact closed and traced symmetric monoidal categories. This encompasses QuantoCosy, a tool for generating rules from models (as set out in [24]), QuantoDerive, a tool for constructing and checking graphical proofs, and QuantoTactic, an Isabelle 31 tactic implementation using Quantomatic's graph-matching engine to direct proofs and checking their correctness in Isabelle.
1 Some initial work on this was done by Matvey Soloviev when the theory of !-graphs and string graphs was still in flux, but nothing was ever published; this could be revisited now that there is a secure foundation.

Appendix A

Correctness of Quantomatic's Matching

We prove the correctness of the algorithm presented in section 7.2 for matching !-graphs onto string graphs.
Recall the match state:
  • L : the pattern graph (normalised)
  • L : an instance of L
  • G : the target graph (normalised)
  • S : a partial instantiation of L ,resulting in L
  • m:VLVG : a partial injective function describing the matching so far
  • UVL : a set of unmatched vertices of L
  • PN(L) : a set of partially-matched node-vertices
  • PSP : a set of schedules partially-matched node-vertices
  • TVG : a set of vertices that can be matched onto
Throughout the entire procedure, in addition to the invariants implicit in the typing of the components of the match state, we maintain the following global invariants:
(1) m is injective and respects vertex types
(2) For any v,wdom(m) ,if there is an edge from v to w in L ,then there is an edge from m(v) to m(w) in G
(3) Pdom(m) and for any node-vertex vdom(m)P ,all wire-vertices adjacent to m(v) in G are in the image of m
Given that !-graphs are simple,invariants (1) and (2) ensure that when m is total,it uniquely extends to a !-graph monomorphism m^:LG . Invariant (3) ensures that,if P is empty, U(m^) will be a local isomorphism. Thus m^ will be a matching of L onto G under S .

A. 1 The String Graph Matching Subroutine

The algorithm is shown in figure A.1.

A.1.1 Preconditions/Invariants

In addition to the global invariants, the string graph matching subroutine has the following require-
ments on the match state. What is more, these are maintained throughout the procedure.
(i) L and G are both normalised
(ii) Udom(m)= (ie: the vertices in the unmatched set are not part of the existing matching)
(iii) Each vertex in UW is adjacent to something in UNPS (ensures we can always reach wire vertices in UW by starting from a node-vertex in UN or PS )
(iv) If vP and NG(m(v))im(m),vPS (everything that is completely matched and in P is also in PS )
(v) If vUW and w is a wire-vertex adjacent to v in L,wUW ( UW contains complete wires)
(vi) If vdom(m) is a wire-vertex,then any vertices it is adjacent to are also in dom(m)
(vii) If vT is a wire-vertex,then any vertices it is adjacent to are in either T or im(m)
(viii) Tim(m)=

A.1.2 Postconditions

These are true for the match state that results from each successful branch:
(I) U=PS= (every vertex marked for matching was handled)
(II) dom(m) is the union of the initial states of U and dom(m) (we have matched exactly what we were asked to)
(III) im(m) contains only vertices that were in either the initial state of im(m) or the initial state of T (matches were only made against vertices in T )
(IV) P is exactly the set of vertices in dom(m) whose image is adjacent to a wire-vertex not in im(m) ( P contains exactly the partially-matched vertices)
(V) L,L,G and S are identical to their starting states
Figure A.1: String Graph Matching Subroutine
Postcondition (II) (in conjunction with the global invariants) states that the algorithm has completed the requested work. Postcondition (1) just states that we left the match state "clean"; it still satisfies all the preconditions and repeating the algorithm without altering the state further would do nothing. Postcondition (IV) says that P is the smallest set that satisfies global invariant (3).

A.1.3 Termination

For termination of the inner loop exploring the wires incident to a node-vertex v ,we consider the variant n=|UWNL(v)| ,where NL(v) is the neighbourhood of v in L . In each of these branches, n decreases by either 1 or 2,and nothing is ever added to UW (and NL(v) is fixed). So this loop must terminate.
The loop working through PS has two branches: when it is not empty and when it is not. Either may add more things to PS . We will take as variant m=2|UN|+|PS| . When this is 0,the algorithm will terminate. Otherwise,if PS is empty, UN will have one vertex removed and added to PS ,decreasing m by one. If PS is not empty,one vertex will be removed from PS ,decreasing m by one. Every vertex that is added to PS in this loop is taken from UN ,further decreasing m . As a result, m will decrease by at least one with every iteration of the loop.

A.1.4 Correctness

There are seven steps of the algorithm that modify the match state; we will show that each of them satisfies the following properties, under the assumption that the preconditions (section A.1.1), global invariants and match state type constraints hold at the start of the step (note that when we say that a vertex is taken from a set, we mean that it was in the set at the start of the step, and is removed from the set by the end of the step):
(a) L,L,G and S are unmodified
(b) If U,T or m are modified,the only modifications are to take vertices from U and extend m to map those vertices to ones of the same type taken from T
(c) If a wire-vertex is added to dom(m) ,then so is the entire wire,and for any pair of vertices u,v in the wire with an edge from u to v ,there is an edge from m(u) to m(v) (at the end of the step) in G
(d) Any vertex taken from UN is added to both P and PS ,and these are the only vertices added to either P or PS
(e) If P or PS are modified,the only modifications are the one from (d),removing a partially matched vertex with no adjacent vertices in UW from PS or removing a completely matched vertex with no adjacent vertices in UW from P and PS
Given that these properties hold, we can show that all steps of the algorithm preserve the match state type constraints, the global invariants and the preconditions.
We can see that (a) holds for all seven steps by inspection. It is clear that the other three properties hold for steps (1)-(3), again by inspection. Only steps (5)-(7) need extra justification. We first note that the selection of w demands that,since L is in normal form,it is part of an interior wire with two wire-vertices or is the input on an input wire or the output on an output wire (and the sole wire-vertex on the wire in both cases).
For step (5), the only non-obvious property is c c). However, by what we have already noted, since w is not on an interior wire it must be an input or output. Since w and v are the only vertices on the wire and v is already in dom(m) ,and the edge between v and w is the same direction as the edge between m(v) and t ,property (c) holds for (5).
In step (6),it is clear that t and t are in T and w is in UW . Precondition (v) ensures that w is in UW . Since L and G are !-graphs, w must have the same type as w ,which has the same type as t ,which has the same type as t . So property (b) clearly holds. Property (c) can be seen to hold by noting that the edge between u and w is in the same direction as the edge between m(u) and t ,and all the edges in a wire must be in the same direction. Properties (d) and (e) trivially hold,as UN , P and PS are not modified.
For step (7), we note that precondition (iii) (together with global invariant 3 and the fact that PSP) requires that,since wUW and uim(m),u must be in UN . Then properties (b) and (c) follow in the same manner as for (6), and properties (d) and (e) clearly hold.
We now show that these properties mean that the match state type constraints, global invariants and preconditions are all maintained.
Type constraints The typing constraints for U and T are trivially maintained as (b) demands they are never changed. Properties (d) and (e) ensure that P is only ever added to from UN and that anything added to PS is also added to P ,and anything removed from P is also removed from PS ,so those constraints hold. Finally,the constraint on m holds by property (b)
Global Invariants Injectivity of m is preserved as property (b) demands that only vertices drawn from T may be used for images of additions to m ,and precondition (viii) gives us that these must
Suppose there is a an edge in L from a vertex v to another vertex w ,and both are in dom(m) at the end of a step, but one was not at the start of the step. We know they cannot both be node-vertices,and so one or both are wire-vertices. Since at least one was not in the image of m at the start of the step, none of the wire-vertices can have been by precondition (vi). Then property (c) ensures that there is an edge from m(v) to m(w) . So global invariant (2) is preserved.
Global invariant (3) is preserved when vertices are removed from P due to property vertices are added to m due to property (b).

Preconditions/Invariants

(i) L and G are both in normal form
By property (a),which ensures L and G are never changed.
(ii) Udom(m)=
Property (b) requires that every vertex added to dom(m) is removed from U .
(iii) Each vertex in UW is adjacent to something in UNPS
Given that property (b) prevents anything being added to UW ,this precondition can only be broken by removing something from UN or PS . Property (d) ensures that anything removed from UN is added to PS ,and property (e) ensures that anything removed from UN has no adjacent vertices in UW .
(iv) If vP and NG(m(v))im(m),vPS
Property (e) ensures that when we add anything to P ,we also add it to PS ,and we only remove completely matched vertices from PS .
(v) If vUW and w is a wire-vertex adjacent to v in L,wUW
Property (c) (in conjunction with property (b)) ensures that only entire wires are removed from UW at once (and nothing is ever added to UW ).
(vi) If vdom(m) is a wire-vertex,then any vertices it is adjacent to are also in dom(m) This is preserved due to property (c).
(vii) If vT is a wire-vertex,then any vertices it is adjacent to are in either T or im(m) This is maintained by property (b),which ensures that anything removed from T is added to im(m) and,due to precondition (ii),also ensures that nothing is ever removed from im(m) .
(viii) Tim(m)=
This is preserved by property (b),which ensures that nothing is ever added to T ,and anything added to im(m) is removed from T .

Postconditions

(I) U=PS=
The conditions that lead to the "done" step ensure that UN and PS are empty. Then precondition (iii) means that UW must be empty. UC is empty at the end because it is empty when step (1) is complete, and property (b) ensures it is never added to.
(II) dom(m) is the union of the initial states of U and dom(m)
Property (b) ensures that everything removed from U is added to m ,that nothing else is added to m and that nothing is removed from m . Combining this with precondition (ii) gives us that no entry of m is every overwritten,and so postcondition (1) provides us with what we need.
(III) im(m) contains only vertices that were in either the initial state of im(m) or the initial state of T By property (b)
(IV) P is exactly the set of vertices in dom(m) whose image is adjacent to a vertex not in im(m) Global invariant (3) gives us most of what we need. We just need that if v is completely matched,it is not in P . But this is guaranteed by invariant (iv) and the fact that PS= .
(V) L,L,G and S are identical to their starting states
This follows immediately from property (a).

Completeness

Let f be a matching of the full subgraph of L given by the vertices Udom(m) into G that restricts to m on the vertices in dom(m) . Then we need to show that,after completion of the algorithm,one of the match states produced will agree with f on vertices,up to a choice of circles. Note that,by the argument at the start of section A,this will then uniquely extend to f .
Since f is a matching with UC in its domain (and UCdom(m)= and f restricts to m ),there must be at least |UC| unmatched circles in G ,and so the step where we match circles must succeed.
Invariant: the vertex map part of f restricts to m.m is extended in two places (after circle-matching). Each of these follows a branching point. We need to show that in both of these places, there is a branch that will maintain this invariant. We also need to show that none of the "die" branches are taken.
When adding something from UN ,it is clear that f(v) is a valid matching for v ,and so this is a branch that will maintain the invariant.
When adding something from UW ,the wire starting f(w) must be a valid matching for the wire starting with w ,as the entire wire must be in the domain of f : if w is an input or output,this is trivial. Otherwise,there must be a wire-vertex w adjacent to w ,and a node-vertex n adjacent to w . Then w is in UW ,and hence in dom(f) ,by precondition 0 v or UN ,by precondition (iii),and so in dom(m) or UN ,and hence n is in dom(f) . Once we have matched w against f(w) ,the only possible matching for w is f(w) ,and similarly n must match against f(n) . If n is already in dom(m) ,we know it maps to f(m) ,so the matchings must agree. So this branch maintains the invariant (and does not die).
Thus,regardless of how vertices are chosen from PS,UN or UW ,there must be a trace that returns a match where m agrees with f on vertices.

A. 2 The Outer Loop

The algorithm is shown in figure A.2. The steps that "apply" a l-box operation implicitly apply the operation to L and record it in S .
Figure A.2: !-graph matching onto string graphs
Note that the global invariants are trivially satisfied at the start of the algorithm,since m and P are empty. They are maintained thereafter as only the string graph matching subroutine and the bare wire matching routines alter m or P ,and the !-box operations (which are the only things to alter L ) can only add edges where either the source or the target is not in dom(m) .

A.2.1 Termination

The algorithm terminates, on the assumption that no sequence of !-box operations will ever produce a wild !-box, by the following argument.
Each step terminates, and there is only one loop. As a variant, we take
n=|VG|+|VLdom(m)||dom(m)|
We calculate the variant at the point where we consider terminating the loop, after the string graph matching step. If the previous iteration involved killing one or more !-boxes, VLdom(m) will decrease (by the combined size of the !-boxes, less bare wires - this amount is positive due to the assumption about wild !-boxes). If the previous iteration involved expanding a !-box, |dom(m)| will increase (by the size of the !-box,excluding any bare wires). VLdom(m) is clearly bounded below by 0,and |dom(m)| is bounded above by |VG| ,by global invariant (1),so n is bounded below by 0 and decreases with every iteration. Hence the algorithm terminates.
Note that Quantomatic's implementation ensures termination for all pattern graphs by killing any wild !-boxes as soon as they are produced.

A.2.2 String Graph Matching Preconditions

We need to show that the preconditions in section A.1.1 are satisfied whenever the string graph matching step is run.
(i) L and G are both normalised
We normalise the graphs at the start. We then do not alter G until the bare wire matching step, at which point the string graph matching routine can no longer be called. Because !-boxes are open subgraphs, operations on them always remove or copy an entire wire at once, which ensures that L remains normalised throughout.
(ii) Udom(m)=
We only ever add unmatched vertices to U .
(iii) Each vertex in UW is adjacent to something in UNPS
This follows from openness of !-boxes, which (together with normalisation) ensures that any wire-vertex in the match surface that is not on a circle or bare wire must be adjacent to a node-vertex in the match surface. The first time string graph matching happens, all such node-vertices are put in UN .
Since all non-bare-wire,non-circle vertices in the match surface are added to UW each time, and so added to dom(m) by the string graph matching step,on subsequent iterations of string graph matching any wire-vertex v in UW must have arisen from the expansion of a !-box (since this is the only way the match surface can be extended). If v is adjacent to a node-vertex that came from the !-box expansion,that node-vertex will be added to UN . Otherwise,it must be adjacent to a node-vertex in dom(m) ,and hence in P (by the postconditions of the string graph matching step). Then this node-vertex (being adjacent to the expanded !-box) will be added to PS .
(iv) If vP and NG(m(v))im(m),vPS (everything that is completely matched and in P is also in PS )
The first time we run the string graph matching step, P is empty. After each string graph matching step,the postconditions ensure that there is no completely matched vertex in P . As the rest of the algorithm does not add anything to P or alter m ,this is maintained throughout.
(v) If vUW and w is a wire-vertex adjacent to v in L,wUW .
This is guaranteed by openness of !-boxes: we only ever add entire wires to UW .
(vi) If vdom(m) is a wire-vertex,then any vertices it is adjacent to are also in dom(m) This is guaranteed by the postcondition (II) in combination with precondition (v) and the fact that m is only altered by the string graph matching step.
(vii) If vT is a wire-vertex,then any vertices it is adjacent to are in either T or im(m)
T and m are only modified by the string graph matching subroutine,which maintains this invariant. Initially, m is empty,causing it to hold trivially.
(viii) Tim(m)=
As above.

A.2.3 Correctness

At the end of the algorithm, everything that was ever in the match surface except for bare wires has been added to m by the string graph matching step (postcondition (II),together with the fact that we always add everything unmatched in the match surface to UW,UC and UN ,except bare wires). We have no more !-boxes,so the entire graph is part of the match surface. P is also empty. We matched bare wires at the last stage,so m is in fact total on L . So,by the argument at the start of section A m is a valid match from the final state of L to G . Since we have only ever performed valid ! -box operations on L ,this is a valid instance of L ,and hence we have found a valid matching from L to G .

A.2.4 Completeness

Providing no instance of L contains a wild !-box (see section 7.1),completeness follows from the fact that any concrete instantiation has an equivalent in expansion-normal form (section 6.2.2).

Appendix B

The Spider Law

The following is joint work with Aleks Kissinger. It is work in progress, as we are still working out the details of the definition style used in this section and intend to extend this to non-commutative generators, as mentioned in section 8.1
Suppose we have a commutative Frobenius algebra in string graph form. So we have the following generators (node-vertices of the typegraph, with their adjacent edges)
where all the edges are fixed-arity, and all the wire-vertices are of the same type. Note that, in the sequel, we will implicitly identify distinguished fixed-arity edges by the position in our presentation of the graph. This is unambiguous with these particular generators, as we can simply count clockwise from the single output of the multiplication node, or the single input of the comultiplication node.
We also have the following equations, where we identify inputs and outputs by position:
It is trivial to use the commutativity laws to derive Suppose we now define a !-boxed version of the multiplication operation in the following manner:
Essentially, we have added a new generator with a variable-arity input and a fixed-arity output, together with rules that allow us to rewrite any instance of it (with any number of incoming edges) into a graph containing only our original set of generators. As noted in section 8.1, this definition assumes associativity and commutativity in order to be consistent.
We now show that a partial form of the spider law holds for variable-arity multiplications.

Lemma B.0.1.

Proof. We proceed by !-box induction. The base case:
and the step case:
We define a variable-arity comultiplication in a similar manner:
:={:=:=:=
and prove a similar result about it:
Lemma B.0.2.
Proof. We proceed by !-box induction. The base case: and the step case:
Now we are ready to define our spider:
And the spider law:
Theorem B.0.3. Proof.
Of course, we need to ensure that our defined spider coincides with the original Frobenius algebra operations:
Theorem B.0.4.

Bibliography

[1] S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 415-425. IEEE, February 2004.
[2] F. Akinniyi, A. C. Wong, and D. Stacey. A new algorithm for graph monomorphism based on the projections of the product graph. IEEE Transactions on Systems, Man, and Cybernetics, 16(5):740-751, September 1986.
[3] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[4] I. Boneva, A. Rensink, M. E. Kurbán, and J. Bauer. Graph abstraction and abstract graph transformation. Technical report, University of Twente, July 2007.
[5] B. Coecke and R. Duncan. Interacting quantum observables: categorical algebra and diagram-matics. New Journal of Physics, 13(4):043016, April 2011.
[6] B. Coecke and A. Kissinger. The compositional structure of multipartite quantum entanglement. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP), volume 6199 of Lecture Notes in Computer Science, pages 297-308. Springer Berlin Heidelberg, February 2010.
[7] B. Coecke, A. Kissinger, A. Merry, and S. Roy. The GHZ/W-calculus contains rational arithmetic. In Proceedings of the CSR 2010 Workshop on High Productivity Computations, volume 52 of Electronic Proceedings in Theoretical Computer Science, pages 34-48, March 2011.
[8] B. Coecke and D. Pavlovic. Quantum measurements without sums. In G. Chen, L. Kauffman, and S. J. Lomonaco, editors, The Mathematics of Quantum Computation and Technology, pages 559-596. Taylor and Francis, August 2007.
[9] L. Dixon and R. Duncan. Graphical reasoning in compact closed categories for quantum computation. Annals of Mathematics and Artificial Intelligence, 56(1):23-42, July 2009.
[10] L. Dixon, R. Duncan, and A. Kissinger. Open graphs and computational reasoning. In Proceedings of the 6th on Developments in Computational Models (DCM), volume 26 of Electronic Proceedings in Theoretical Computer Science, pages 169-180, June 2010.
[11] L. Dixon and A. Kissinger. Open-graphs and monoidal theories. Mathematical Structures in Computer Science, 23(2):308-359, February 2013.
[12] R. Duncan and M. Lucas. Verifying the Steane code with Quantomatic. In Proceedings of the 10th International Workshop on Quantum Physics and Logic (QPL), 2013.
[13] R. Duncan and S. Perdrix. Rewriting measurement-based quantum computations with generalised flow. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP), volume 6199 of Lecture Notes in Computer Science, pages 285-296. Springer Berlin Heidelberg, 2010.
[14] H. Ehrig and H.-J. Kreowski. Church-Rosser theorems leading to parallel and canonical derivations for graph-grammars. Technical report, TU Berlin, 1975.
[15] H. Ehrig, M. Pfender, and H. J. Schneider. Graph-grammars: an algebraic approach. In Conference Record of the 14th Annual Symposium on Switching and Automata Theory (SWAT), pages 167-180. IEEE, October 1973.
[16] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987.
[17] D. Gries and F. B. Schneider. A Logical Approach to Discrete Mathematics. Springer Verlag, 1993.
[18] M. Hasegawa, M. Hofmann, and G. Plotkin. Finite dimensional vector spaces are complete for traced symmetric monoidal categories. In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of Computer Science, Lecture Notes in Computer Science, pages 367-385. Springer Berlin Heidelberg, 2008.
[19] G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23(1):11-21, August 1981.
[20] A. Joyal and R. Street. The geometry of tensor calculus I. Advances in Mathematics, 88(1):55- 112, July 1991.
[21] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(03):447-468, April 1996.
[22] A. Kissinger. Graph rewrite systems for classical structures in -symmetric monoidal categories. MSc Thesis, University of Oxford, 2008.
[23] A. Kissinger. Pictures of Processes. DPhil Thesis, University of Oxford, 2011.
[24] A. Kissinger. Synthesising graphical theories. In Proceedings of the 1st Workshop on Automated Theory eXploration (ATX), February 2012.
[25] A. Kissinger, A. Merry, L. Dixon, R. Duncan, M. Soloviev, and B. Frot. Quantomatic, https://sites.google.com/site/quantomatic/.
[26] A. Kissinger, A. Merry, and M. Soloviev. Pattern graph rewrite systems. In Proceedings of the 8th International Workshop on Developments in Computational Models (DCM), Electronic Proceedings in Theoretical Computer Science, 2012.
[27] S. Lack and P. Sobociński. Adhesive and quasiadhesive categories. Theoretical Informatics and Applications, 39(3):511-545, 2005.
[28] A. Lang and B. Coecke. Trichromatic open digraphs for understanding qubits. In Proceedings of the 8th International Workshop on Quantum Physics and Logic (QPL), volume 95 of Electronic Proceedings in Theoretical Computer Science, pages 193-209, October 2011.
[29] S. Mac Lane. Categories for the Working Mathematician. Springer Verlag, 2nd edition, 1998.
[30] U. Nickel, J. Niere, and A. Zündorf. The FuJaBa environment. In Proceedings of the 22nd International Conference on Software Engineering (ICSE), pages 742-745, 2000.
[31] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2002.
[32] R. Penrose. Applications of negative dimensional tensors. In D. J. A. Welsh, editor, Combinatorial Mathematics and its Applications, pages 221-244. Academic Press, New York, New York, USA, 1971.
[33] J. L. Pfaltz and A. Rosenfeld. Web grammars. In Proceedings of the 1st International Joint Conference on Artificial Intelligence, pages 609-619. Morgan Kaufmann Publishers Inc., 1969.
[34] A. Rensink. Nested quantification in graph transformation rules. In Proceedings of the 3rd International Conference on Graph Transformations (ICGT), volume 4178 of Lecture Notes in Computer Science, pages 1-13. Springer Berlin Heidelberg, September 2006.
[35] A. Rensink and J.-H. Kuperus. Repotting the geraniums: on nested graph transformation rules. Electronic Communications of the EASST, 18, 2009.
[36] H. J. Schneider. Chomsky-Systeme für partielle Ordnungen. Technical report, Universität Erlangen, 1970.
[37] P. Selinger. A survey of graphical languages for monoidal categories. In B. Coecke, editor, New Structures for Physics, volume 813, pages 289-355. Springer Berlin Heidelberg, August 2009.
[38] F. Stallmann. A model-driven approach to multi-agent system design. PhD Thesis, University of Paderborn, 2008.
[39] G. Taentzer. Parallel and distributed graph transformation: formal description and application to communication-based systems. PhD Thesis, TU Berlin, 1996.
[40] J. R. Ullmann. An algorithm for subgraph isomorphism. Journal of the ACM, 23(1):31-42, January 1976.
[41] P. M. van den Broek. Algebraic graph rewriting using a single pushout. In Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 493 of Lecture Notes in Computer Science, pages 90-102. Springer Berlin Heidelberg, 1991.